当递减参数是函数的命名参数时，可以通过引用其名称来指定。

def half (n : Nat) : Nat := match n with | 0 | 1 => 0 | n + 2 => half n + 1 termination_by structural n

当签名中未命名递减参数时，可以在 Lean.Parser.Command.declaration : commandtermination_by 子句中本地引入名称。

def half : Nat → Nat | 0 | 1 => 0 | n + 2 => half n + 1 termination_by structural n => n

递减参数的类型必须是归纳类型。 在notInductive中，指定了一个函数作为递减参数：

def notInductive (x : Nat → Nat) : Nat := notInductive (fun n => x (n+1)) cannot use specified measure for structural recursion: its type is not an inductivetermination_by structural x

cannot use specified measure for structural recursion:
  its type is not an inductive

如果递减参数是索引族，则所有索引都必须是变量。 在 constantIndex 中，索引系列 Fin' 改为应用于常量值：

inductive Fin' : Nat → Type where | zero : Fin' (n+1) | succ : Fin' n → Fin' (n+1) def constantIndex (x : Fin' 100) : Nat := constantIndex .zero cannot use specified measure for structural recursion: its type Fin' is an inductive family and indices are not variables Fin' 100termination_by structural x

cannot use specified measure for structural recursion:
  its type Fin' is an inductive family and indices are not variables
    Fin' 100

递减参数类型的参数不得依赖于变化参数或索引之后的函数参数。 在afterVarying中，固定前缀为空，因为第一个参数n变化，所以p不是固定前缀的一部分：

inductive WithParam' (p : Nat) : Nat → Type where | zero : WithParam' p (n+1) | succ : WithParam' p n → WithParam' p (n+1) failed to infer structural recursion: Cannot use parameter x: failed to eliminate recursive application afterVarying (n + 1) p WithParam'.zero def afterVarying (n : Nat) (p : Nat) (x : WithParam' p n) : Nat := afterVarying (n+1) p .zero termination_by structural x

failed to infer structural recursion:
Cannot use parameter x:
  failed to eliminate recursive application
    afterVarying (n + 1) p WithParam'.zero

在以下示例中，递减参数 n 与嵌套模式 .succ (.succ n) 进行匹配。因此，.succ (.succ n) 是 n 的（非严格）子术语，因此 n 和 .succ n 都是严格子术语，并且定义被接受。

def fib : Nat → Nat | 0 | 1 => 1 | .succ (.succ n) => fib n + fib (.succ n) termination_by structural n => n

为清楚起见，本示例使用 .succ n 和 .succ (.succ n)，而不是等效的 Nat 特定的 n+1 和 n+2。

在以下示例中，递减参数 n 并不直接是 Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not. match 表达式的 判别式。 因此，n' 不被视为 n 的子术语。

failed to infer structural recursion: Cannot use parameter n: failed to eliminate recursive application half n' def half (n : Nat) : Nat := match Option.some n with | .some (n' + 2) => half n' + 1 | _ => 0 termination_by structural n

failed to infer structural recursion:
Cannot use parameter n:
  failed to eliminate recursive application
    half n'

使用 良基递归，并将判别式显式连接到匹配模式，可以接受此定义。

def half (n : Nat) : Nat := match h : Option.some n with | .some (n' + 2) => half n' + 1 | _ => 0 termination_by n decreasing_by simp_alln:Natn':Nath:n = n' + 1 + 1⊢ n' < n' + 1 + 1; omegaAll goals completed! 🐙

同样，以下示例失败：尽管 xs.tail 会简化为 xs 的严格子项，但根据上述规则，这对 Lean 不可见。 特别是，xs.tail 不 定义等于 xs 的严格子项。

failed to infer structural recursion: Cannot use parameter #2: failed to eliminate recursive application listLen xs.tail def listLen : List α → Nat | [] => 0 | xs => listLen xs.tail + 1 termination_by structural xs => xs

用于证明终止的策略的一个重要结果是两个 判别式的同时匹配并不等于匹配一对。 同时匹配保持判别式和模式之间的联系，允许模式匹配细化本地上下文中的假设类型以及 Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not. match 的预期类型。 本质上，Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given term `e` against each pattern `p` of a match alternative. When all patterns of an alternative match, the `match` term evaluates to the value of the corresponding right-hand side `f` with the pattern variables bound to the respective matched values. If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available within `f`. When not constructing a proof, `match` does not automatically substitute variables matched on in dependent variables' types. Use `match (generalizing := true) ...` to enforce this. Syntax quotations can also be used in a pattern match. This matches a `Syntax` value against quotations, pattern variables, or `_`. Quoted identifiers only match identical identifiers - custom matching such as by the preresolved names only should be done explicitly. `Syntax.atom`s are ignored during matching by default except when part of a built-in literal. For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they should participate in matching. For example, in ```lean syntax "c" ("foo" <|> "bar") ... ``` `foo` and `bar` are indistinguishable during matching, but in ```lean syntax foo := "foo" syntax "c" (foo <|> "bar") ... ``` they are not. match 的精化规则会特殊对待判别式，并且以保留程序运行时含义的方式更改判别式不一定会保留编译时含义。

此函数查找两个自然数中的最小值，由结构递归在其第一个参数上定义：

def min' (n k : Nat) : Nat := match n, k with | 0, _ => 0 | _, 0 => 0 | n' + 1, k' + 1 => min' n' k' + 1 termination_by structural n

将两个参数上的同时模式匹配替换为一对上的匹配会导致终止分析失败：

failed to infer structural recursion: Cannot use parameter n: failed to eliminate recursive application min' n' k' def min' (n k : Nat) : Nat := match (n, k) with | (0, _) => 0 | (_, 0) => 0 | (n' + 1, k' + 1) => min' n' k' + 1 termination_by structural n

failed to infer structural recursion:
Cannot use parameter n:
  failed to eliminate recursive application
    min' n' k'

这是因为当将递归调用与严格较小的参数值匹配时，分析仅考虑参数上的直接模式匹配。 将判别式包装成一对会破坏连接。

无法通过结构递归详细说明此函数，该函数用于查找一对的两个分量中的最小值。

failed to infer structural recursion: Cannot use parameter nk: the type Nat × Nat does not have a `.brecOn` recursor def min' (nk : Nat × Nat) : Nat := match nk with | (0, _) => 0 | (_, 0) => 0 | (n' + 1, k' + 1) => min' (n', k') + 1 termination_by structural nk

failed to infer structural recursion:
Cannot use parameter nk:
  the type Nat × Nat does not have a `.brecOn` recursor

这是因为参数的类型 Prod 不是递归的。 因此，其构造函数没有可由模式匹配公开的递归参数。

使用 良基递归 可以接受此定义，但是：

def min' (nk : Nat × Nat) : Nat := match nk with | (0, _) => 0 | (_, 0) => 0 | (n' + 1, k' + 1) => min' (n', k') + 1 termination_by nk

即使 countdown 的递归出现应用于不是递减参数的严格子项的项，也接受以下定义：

def countdown (n : Nat) : List Nat := match n with | 0 => [] | n' + 1 => n' :: countdown (n' + 0) termination_by structural n

这是因为 n' + 0 是 定义等于 n'，这是 n 的严格子术语。 从模式匹配生成的 子项 使用 匹配泛化 的规则连接到 判别，该规则尊重 定义等价。

在 countdown' 中，递归出现应用于 0 + n'，它在定义上并不等于 n'，因为自然数上的加法在其第二个参数中是结构递归的：

failed to infer structural recursion: Cannot use parameter n: failed to eliminate recursive application countdown' (0 + n') def countdown' (n : Nat) : List Nat := match n with | 0 => [] | n' + 1 => n' :: countdown' (0 + n') termination_by structural n

failed to infer structural recursion:
Cannot use parameter n:
  failed to eliminate recursive application
    countdown' (0 + n')

以下示例演示了非互归纳数据类型上的相互递归：

mutual def even : Nat → Prop | 0 => True | n+1 => odd n termination_by structural n => n def odd : Nat → Prop | 0 => False | n+1 => even n termination_by structural n => n end

以下示例演示了相互归纳类型上的递归。 函数 Exp.size 和 App.size 是相互递归的。

mutual inductive Exp where | var : String → Exp | app : App → Exp inductive App where | fn : String → App | app : App → Exp → App end mutual def Exp.size : Exp → Nat | .var _ => 1 | .app a => a.size termination_by structural e => e def App.size : App → Nat | .fn _ => 1 | .app a e => a.size + e.size + 1 termination_by structural a => a end

App.numArgs 的定义在类型 App 上进行结构递归。 说明并非交互组中的所有归纳类型都需要处理。

def App.numArgs : App → Nat | .fn _ => 0 | .app a _ => a.numArgs + 1 termination_by structural a => a

Lean 自动推断函数 half 在结构上是递归的。 termination_by? 子句会导致显示推断的终止注释，并且只需单击一下即可将其自动添加到源文件中。

def half : Nat → Nat | 0 | 1 => 0 | n + 2 => half n + 1 Try this: [apply] termination_by structural x => xtermination_by?

Try this:
  [apply] termination_by structural x => x

自然数的添加可以通过第二个参数的递归来定义。 该函数在结构上是直接递归的。

def add (n : Nat) : Nat → Nat | .zero => n | .succ k => .succ (add n k)

使用 Nat.rec 定义，它与大多数人习惯的符号相距甚远。

def add' (n : Nat) := Nat.rec (motive := fun _ => Nat) n (fun Variable name `k` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`k soFar => .succ soFar)

对不是函数参数的直接子代的数据进行的结构递归调用需要创造力或复杂但系统的编码。

def half : Nat → Nat | 0 | 1 => 0 | n + 2 => half n + 1

将此函数视为结构递归，它在每次调用时翻转一位，仅在设置该位时递增结果。

def helper : Nat → Bool → Nat := Nat.rec (motive := fun _ => Bool → Nat) (fun _ => 0) (fun _ soFar => fun b => (if b then Nat.succ else id) (soFar !b)) def half' (n : Nat) : Nat := helper n false [0, 0, 1, 1, 2, 2, 3, 3, 4]#eval [0, 1, 2, 3, 4, 5, 6, 7, 8].map half'

[0, 0, 1, 1, 2, 2, 3, 3, 4]

可以使用称为 值过程递归 的通用技术来代替创造力。 值过程递归使用可以为每个归纳类型系统导出的帮助程序，根据递归器定义； Lean 自动导出它们。 对于每个 Nat n，类型 n.below (motive := mot) 为所有 k < n 提供 mot k 类型的值，表示为迭代的 相关对类型。 值过程递归器 Nat.brecOn 允许函数使用任何较小的 Nat 的结果。 用它来定义函数很不方便：

noncomputable def half'' (n : Nat) : Nat := Nat.brecOn n (motive := fun _ => Nat) fun k soFar => match k, soFar with | 0, _ | 1, _ => 0 | _ + 2, ⟨_, ⟨h, _⟩⟩ => h + 1

该函数被标记为 Lean.Parser.Command.declaration : commandnoncomputable，因为编译器不支持生成值过程递归的代码，该递归旨在用于推理而不是高效的代码。 内核仍可用于测试该功能，但是：

[0, 0, 1, 1, 2, 2, 3, 3, 4]#reduce [0,1,2,3,4,5,6,7,8].map half''

[0, 0, 1, 1, 2, 2, 3, 3, 4]

如果需要，half'' 主体中的依赖模式匹配也可以使用递归器（具体来说，Nat.casesOn）进行编码：

noncomputable def half''' (n : Nat) : Nat := n.brecOn (motive := fun _ => Nat) fun k => k.casesOn (motive := fun k' => (k'.below (motive := fun _ => Nat)) → Nat) (fun _ => 0) (fun k' => k'.casesOn (motive := fun k'' => (k''.succ.below (motive := fun _ => Nat)) → Nat) (fun _ => 0) (fun _ soFar => soFar.2.1.succ))

这个定义仍然有效。

[0, 0, 1, 1, 2, 2, 3, 3, 4]#reduce [0,1,2,3,4,5,6,7,8].map half''

[0, 0, 1, 1, 2, 2, 3, 3, 4]

然而，现在它与最初的定义相去甚远，对于大多数人来说已经变得难以理解。 递归是一个很好的逻辑基础，但不是编写程序或证明的简单方法。

该定义等价于 List.below：

def List.below' {α : Type u} {motive : List α → Sort u} : List α → Sort (max (u + 1) u) | [] => PUnit | _ :: xs => motive xs ×' xs.below' (motive := motive)

换句话说，对于给定的 motive，List.below' 是包含列表中所有后缀的动机实现的类型。

更多的递归参数需要产品类型的进一步嵌套迭代。 例如，二叉树有两次递归出现。

inductive Tree (α : Type u) : Type u where | leaf | branch (left : Tree α) (val : α) (right : Tree α)

其对应的值过程表包含所有子树动机的实现：

def Tree.below' {α : Type u} {motive : Tree α → Sort u} : Tree α → Sort (max (u + 1) u) | .leaf => PUnit | .branch left _val right => (motive left ×' left.below' (motive := motive)) ×' (motive right ×' right.below' (motive := motive))

对于列表和树，brecOn 运算符只需要一种情况，而不是每个构造函数一种情况。 这种情况接受一个列表或树以及所有较小值的结果表；由此看来，它应该满足提供价值的动机。 对所提供值的相关案例分析会自动细化备注表的类型，提供所需的一切。

以下定义分别相当于 List.brecOn 和 Tree.brecOn。 原始递归助手 List.brecOnTable 和 Tree.brecOnTable 计算值过程表以及最终结果，而 brecOn 运算符的实际定义只是投影出结果。

def List.brecOnTable {α : Type u} {motive : List α → Sort u} (xs : List α) (step : (ys : List α) → ys.below' (motive := motive) → motive ys) : motive xs ×' xs.below' (motive := motive) := match xs with | [] => ⟨step [] PUnit.unit, PUnit.unit⟩ | x :: xs => let res := xs.brecOnTable (motive := motive) step let val := step (x :: xs) res ⟨val, res⟩ def Tree.brecOnTable {α : Type u} {motive : Tree α → Sort u} (t : Tree α) (step : (ys : Tree α) → ys.below' (motive := motive) → motive ys) : motive t ×' t.below' (motive := motive) := match t with | .leaf => ⟨step .leaf PUnit.unit, PUnit.unit⟩ | .branch left val right => let resLeft := left.brecOnTable (motive := motive) step let resRight := right.brecOnTable (motive := motive) step let branchRes := ⟨resLeft, resRight⟩ let val := step (.branch left val right) branchRes ⟨val, branchRes⟩ def List.brecOn' {α : Type u} {motive : List α → Sort u} (xs : List α) (step : (ys : List α) → ys.below' (motive := motive) → motive ys) : motive xs := (xs.brecOnTable (motive := motive) step).1 def Tree.brecOn' {α : Type u} {motive : Tree α → Sort u} (t : Tree α) (step : (ys : Tree α) → ys.below' (motive := motive) → motive ys) : motive t := (t.brecOnTable (motive := motive) step).1

遍历 half 的精化的第一步是将其手动脱糖为更简单的形式。 这与 Lean 的工作方式不匹配，但当存在的 OfNat 实例较少时，其输出更容易阅读。 这个可读的定义：

def half : Nat → Nat | 0 | 1 => 0 | n + 2 => half n + 1

可以重写为这个较低级别的版本：

def half : Nat → Nat | .zero | .succ .zero => .zero | .succ (.succ n) => half n |>.succ

精化器首先精化了一个预定义，其中递归仍然存在，但定义在 Lean 的核心 类型论 中。 打开编译器对预定义的跟踪，并使漂亮的打印机更加明确，使生成的预定义可见：

set_option trace.Elab.definition.body true in set_option pp.all true in [Elab.definition.body] half : Nat → Nat := fun (x : Nat) => half.match_1.{1} (fun (x : Nat) => Nat) x (fun (_ : Unit) => Nat.zero) (fun (_ : Unit) => Nat.zero) fun (n : Nat) => Nat.succ (half n)def half : Nat → Nat | .zero | .succ .zero => .zero | .succ (.succ n) => half n |>.succ

返回的跟踪消息是：

[Elab.definition.body] half : Nat → Nat :=
    fun (x : Nat) =>
      half.match_1.{1} (fun (x : Nat) => Nat) x
        (fun (_ : Unit) => Nat.zero)
        (fun (_ : Unit) => Nat.zero)
        fun (n : Nat) => Nat.succ (half n)

辅助匹配函数的定义为：

@[implicit_reducible] def half.match_1.{u_1} : (motive : Nat → Sort u_1) → (x : Nat) → (Unit → motive Nat.zero) → (Unit → motive 1) → ((n : Nat) → motive n.succ.succ) → motive x := fun motive x h_1 h_2 h_3 => Nat.casesOn x (h_1 ()) fun n => Nat.casesOn n (h_2 ()) fun n => h_3 n#print half.match_1

@[implicit_reducible] def half.match_1.{u_1} : (motive : Nat → Sort u_1) →
  (x : Nat) → (Unit → motive Nat.zero) → (Unit → motive 1) → ((n : Nat) → motive n.succ.succ) → motive x :=
fun motive x h_1 h_2 h_3 => Nat.casesOn x (h_1 ()) fun n => Nat.casesOn n (h_2 ()) fun n => h_3 n

格式更易读，这个定义是：

def half.match_1'.{u} : (motive : Nat → Sort u) → (x : Nat) → (Unit → motive Nat.zero) → (Unit → motive 1) → ((n : Nat) → motive n.succ.succ) → motive x := fun Variable name `motive` is not explicitly referenced. The binding can be removed (if unused) or named `_` (if used implicitly). Note: This linter can be disabled with `set_option linter.unusedVariables false`motive x h_1 h_2 h_3 => Nat.casesOn x (h_1 ()) fun n => Nat.casesOn n (h_2 ()) fun n => h_3 n

换句话说，half 中使用的模式的具体配置在 half.match_1 中捕获。

该定义是 half 预定义的更具可读性的版本：

def half' : Nat → Nat := fun (x : Nat) => half.match_1 (motive := fun _ => Nat) x (fun _ => 0) -- Case for 0 (fun _ => 0) -- Case for 1 (fun n => Nat.succ (half' n)) -- Case for n + 2

要将其精化为结构递归函数，第一步是建立 bRecOn 调用。 该定义必须标记为 Lean.Parser.Command.declaration : commandnoncomputable，因为 Lean 不支持递归器（例如 Nat.brecOn）的代码生成。

noncomputable def half'' : Nat → Nat := fun (x : Nat) => x.brecOn fun n table => don't know how to synthesize placeholder context: x n:Nattable:Nat.below n⊢ Nat_ /- To translate: half.match_1 (motive := fun _ => Nat) x (fun _ => 0) -- Case for 0 (fun _ => 0) -- Case for 1 (fun n => Nat.succ (half' n)) -- Case for n + 2 -/

下一步是将原始函数体中出现的 x 替换为 brecOn 提供的 n。 由于 table 的类型取决于 x，因此在使用 half.match_1 拆分案例时也必须对其进行泛化，从而导致带有额外参数的动机。

noncomputable def half'' : Nat → Nat := fun (x : Nat) => x.brecOn fun n table => (half.match_1 (motive := fun k => k.below (motive := fun _ => Nat) → Nat) n don't know how to synthesize placeholder for argument `h_1` context: x n:Nattable:Nat.below n⊢ Unit → Nat.below Nat.zero → Nat_ don't know how to synthesize placeholder for argument `h_2` context: x n:Nattable:Nat.below n⊢ Unit → Nat.below 1 → Nat_ don't know how to synthesize placeholder for argument `h_3` context: x n:Nattable:Nat.below n⊢ (n : Nat) → Nat.below n.succ.succ → Nat_) table /- To translate: (fun _ => 0) -- Case for 0 (fun _ => 0) -- Case for 1 (fun n => Nat.succ (half' n)) -- Case for n + 2 -/

这三种情况的占位符需要以下类型：

don't know how to synthesize placeholder for argument `h_1`
context:
x n:Nattable:Nat.below n⊢ Unit → Nat.below Nat.zero → Nat

don't know how to synthesize placeholder for argument `h_2`
context:
x n:Nattable:Nat.below n⊢ Unit → Nat.below 1 → Nat

don't know how to synthesize placeholder for argument `h_3`
context:
x n:Nattable:Nat.below n⊢ (n : Nat) → Nat.below n.succ.succ → Nat

预定义中的前两种情况是常量函数，无需检查递归：

noncomputable def half'' : Nat → Nat := fun (x : Nat) => x.brecOn fun n table => (half.match_1 (motive := fun k => k.below (motive := fun _ => Nat) → Nat) n (fun () _ => .zero) (fun () _ => .zero) don't know how to synthesize placeholder for argument `h_3` context: x n:Nattable:Nat.below n⊢ (n : Nat) → Nat.below n.succ.succ → Nat_) table /- To translate: (fun n => Nat.succ (half' n)) -- Case for n + 2 -/

最后一种情况包含递归调用。 它应该转换为对值过程表的查找。 最后一个孔类型的更易读的表示是：

(n : Nat) → Nat.below (motive := fun _ => Nat) n.succ.succ → Nat

这相当于

(n : Nat) → Nat ×' (Nat ×' Nat.below (motive := fun _ => Nat) n) → Nat

值过程表中的第一个 Nat 是 n + 1 的递归结果，第二个是 n 的递归结果。 因此，递归调用可以替换为查找，并且精化成功：

noncomputable def half'' : Nat → Nat := fun (x : Nat) => x.brecOn fun n table => (half.match_1 (motive := fun k => k.below (motive := fun _ => Nat) → Nat) n (fun () _ => .zero) (fun () _ => .zero) (fun _ table => Nat.succ table.2.1) table unexpected end of input; expected ')', ',' or ':'

实际的精化器通过将具有新名称的哨兵类型插入到动机中来跟踪为结构递归检查的参数与值过程表中的位置之间的关系。

一般来说，函数类型不具有对终止证明有用的有根据的关系。 实例综合因此选择instSizeOfDefault和相应的有根据的关系。 如果度量是函数，则选择默认的 SizeOf 实例，证明无法成功。

declaration uses `sorry`def declaration uses `sorry`fooInst (b : Bool → Bool) : Unit := fooInst (b ∘ b) termination_by b decreasing_by guard_target = @sizeOf (Bool → Bool) (instSizeOfDefault _) (b ∘ b) < sizeOf bb:Bool → Bool⊢ sizeOf (b ∘ b) < sizeOf b simp only [sizeOf, default.sizeOf]b:Bool → Bool⊢ 0 < 0 guard_target = 0 < 0b:Bool → Bool⊢ 0 < 0 simpb:Bool → Bool⊢ False guard_target = Falseb:Bool → Bool⊢ False sorryAll goals completed! 🐙

以下斐波那契数列的递归定义有两次递归调用，这导致终止证明中有两个目标。

def fib (n : Nat) := if h : n ≤ 1 then 1 else fib (n - 1) + fib (n - 2) termination_by n unsolved goals n:Nath:¬n ≤ 1⊢ n - 1 < n n:Nath:¬n ≤ 1⊢ n - 2 < ndecreasing_by skipn:Nath:¬n ≤ 1⊢ n - 1 < nn:Nath:¬n ≤ 1⊢ n - 2 < n

这里，measure 只是参数本身，有根据的顺序是自然数上的小于关系。 第一个证明目标要求用户证明第一个递归调用的参数（即 n - 1）严格小于函数的参数 n。

两种端接证明均可使用 omega策略轻松解除。

def fib (n : Nat) := if h : n ≤ 1 then 1 else fib (n - 1) + fib (n - 2) termination_by n decreasing_by ·n:Nath:¬n ≤ 1⊢ n - 1 < n omegaAll goals completed! 🐙 ·n:Nath:¬n ≤ 1⊢ n - 2 < n omegaAll goals completed! 🐙