比较文本

查找两个文本文件之间的差异

实时编辑器

折叠未更改行

关闭换行

视图

比对精度

语法高亮

Diffchecker Desktop 运行Diffchecker最安全的方式。获取Diffchecker桌面应用：您的差异永远不会离开您的电脑！获取桌面版

TCTree

创建于去年差异永不过期

60 删除

行
总计
删除

字符
总计
删除

要继续使用此功能，请升级到 Diffchecker Pro 查看价格

153 行

41 添加

行
总计
添加

字符
总计
添加

要继续使用此功能，请升级到 Diffchecker Pro 查看价格

137 行

def TCTree._sizeOf_2 : (I : Prop) × (I → TCTree) → ℕ :=

def TCTree._sizeOf_2 : (I : Type 1) × (I → TCTree) → ℕ :=

fun t => TCTree.rec_1 (fun a a_ih => 1 + a_ih) (fun fst snd snd_ih => 1 + sizeOf fst) t

protected def TCTree.noConfusionType.{u} : Sort u → TCTree → TCTree → Sort u :=

fun P x1 x2 => x1.casesOn fun a => TCTree.noConfusionType.withCtor (Sort u) 0 (fun x a_1 => (a = a_1 → P) → P) P x2

protected def TCTree.brecOn.{u} : {motive_1 : TCTree → Sort u} →

protected axiom TCTree.brecOn.{u} : {motive_1 : TCTree → Sort u} →

{motive_2 : (I : Prop) × (I → TCTree) → Sort u} →

{motive_2 : (I : Type 1) × (I → TCTree) → Sort u} →

(t : TCTree) →

((t : TCTree) → t.below → motive_1 t) →

((t : (I : Prop) × (I → TCTree)) → TCTree.below_1 t → motive_2 t) → motive_1 t :=

((t : (I : Type 1) × (I → TCTree)) → TCTree.below_1 t → motive_2 t) → motive_1 t

fun {motive_1} {motive_2} t F_1 F_2 =>

(TCTree.rec (fun a a_ih => ⟨F_1 (TCTree.node a) a_ih, a_ih⟩)

(fun fst snd snd_ih =>

⟨F_2 ⟨fst, snd⟩ ⟨fun a => (snd_ih a).1, fun a => (snd_ih a).2⟩, fun a => (snd_ih a).1, fun a => (snd_ih a).2⟩)

t).1

protected def TCTree.below.{u} : {motive_1 : TCTree → Sort u} →

protected axiom TCTree.below.{u} : {motive_1 : TCTree → Sort u} →

{motive_2 : (I : Prop) × (I → TCTree) → Sort u} → TCTree → Sort (max 1 u) :=

{motive_2 : (I : Type 1) × (I → TCTree) → Sort u} → TCTree → Sort (max 1 u)

fun {motive_1} {motive_2} t =>

TCTree.rec (fun a a_ih => motive_2 a ×' a_ih)

(fun fst snd snd_ih => ((a : fst) → motive_1 (snd a)) ×' ((a : fst) → snd_ih a)) t

protected def TCTree.noConfusionType.withCtorType.{u} : Type u → ℕ → Type (max 1 u) :=

protected def TCTree.noConfusionType.withCtorType.{u} : Type u → ℕ → Type (max 3 u) :=

fun P ctorIdx => PUnit.{2} → (I : Prop) × (I → TCTree) → P

fun P ctorIdx => PUnit.{4} → (I : Type 1) × (I → TCTree) → P

constructor TCTree.node : (I : Prop) × (I → TCTree) → TCTree

constructor TCTree.node : (I : Type 1) × (I → TCTree) → TCTree

protected def TCTree.binductionOn_1 : ∀ {motive_1 : TCTree → Prop} {motive_2 : (I : Prop) × (I → TCTree) → Prop}

protected def TCTree.binductionOn_1 : ∀ {motive_1 : TCTree → Prop} {motive_2 : (I : Type 1) × (I → TCTree) → Prop}

(t : (I : Prop) × (I → TCTree)),

(t : (I : Type 1) × (I → TCTree)),

(∀ (t : TCTree), t.ibelow → motive_1 t) →

(∀ (t : (I : Prop) × (I → TCTree)), TCTree.ibelow_1 t → motive_2 t) → motive_2 t :=

(∀ (t : (I : Type 1) × (I → TCTree)), TCTree.ibelow_1 t → motive_2 t) → motive_2 t :=

fun {motive_1} {motive_2} t F_1 F_2 =>

(TCTree.rec_1 (fun a a_ih => ⟨F_1 (TCTree.node a) a_ih, a_ih⟩)

(fun fst snd snd_ih =>

⟨F_2 ⟨fst, snd⟩ ⟨fun a => (snd_ih a).1, fun a => (snd_ih a).2⟩, ⟨fun a => (snd_ih a).1, fun a => (snd_ih a).2⟩⟩)

t).1

protected def TCTree.brecOn_1.{u} : {motive_1 : TCTree → Sort u} →

protected axiom TCTree.brecOn_1.{u} : {motive_1 : TCTree → Sort u} →

{motive_2 : (I : Prop) × (I → TCTree) → Sort u} →

{motive_2 : (I : Type 1) × (I → TCTree) → Sort u} →

(t : (I : Prop) × (I → TCTree)) →

(t : (I : Type 1) × (I → TCTree)) →

((t : TCTree) → t.below → motive_1 t) →

((t : (I : Prop) × (I → TCTree)) → TCTree.below_1 t → motive_2 t) → motive_2 t :=

((t : (I : Type 1) × (I → TCTree)) → TCTree.below_1 t → motive_2 t) → motive_2 t

fun {motive_1} {motive_2} t F_1 F_2 =>

(TCTree.rec_1 (fun a a_ih => ⟨F_1 (TCTree.node a) a_ih, a_ih⟩)

(fun fst snd snd_ih =>

⟨F_2 ⟨fst, snd⟩ ⟨fun a => (snd_ih a).1, fun a => (snd_ih a).2⟩, fun a => (snd_ih a).1, fun a => (snd_ih a).2⟩)

t).1

protected def TCTree.binductionOn : ∀ {motive_1 : TCTree → Prop} {motive_2 : (I : Prop) × (I → TCTree) → Prop}

protected def TCTree.binductionOn : ∀ {motive_1 : TCTree → Prop} {motive_2 : (I : Type 1) × (I → TCTree) → Prop}

(t : TCTree),

(∀ (t : TCTree), t.ibelow → motive_1 t) →

(∀ (t : (I : Prop) × (I → TCTree)), TCTree.ibelow_1 t → motive_2 t) → motive_1 t :=

(∀ (t : (I : Type 1) × (I → TCTree)), TCTree.ibelow_1 t → motive_2 t) → motive_1 t :=

fun {motive_1} {motive_2} t F_1 F_2 =>

(TCTree.rec (fun a a_ih => ⟨F_1 (TCTree.node a) a_ih, a_ih⟩)

(fun fst snd snd_ih =>

⟨F_2 ⟨fst, snd⟩ ⟨fun a => (snd_ih a).1, fun a => (snd_ih a).2⟩, ⟨fun a => (snd_ih a).1, fun a => (snd_ih a).2⟩⟩)

t).1

def TCTree.casesOn.{u} : {motive_1 : TCTree → Sort u} →

(t : TCTree) → ((a : (I : Prop) × (I → TCTree)) → motive_1 (TCTree.node a)) → motive_1 t :=

(t : TCTree) → ((a : (I : Type 1) × (I → TCTree)) → motive_1 (TCTree.node a)) → motive_1 t :=

fun {motive_1} t node => TCTree.rec (fun a a_ih => node a) (fun fst snd snd_ih => PUnit.unit) t

theorem TCTree.node.sizeOf_spec : ∀ (a : (I : Prop) × (I → TCTree)), sizeOf (TCTree.node a) = 1 + sizeOf a :=

theorem TCTree.node.sizeOf_spec : ∀ (a : (I : Type 1) × (I → TCTree)), sizeOf (TCTree.node a) = 1 + sizeOf a :=

fun a => Eq.refl (1 + sizeOf a)

recursor TCTree.rec_1.{u} : {motive_1 : TCTree → Sort u} →

{motive_2 : (I : Prop) × (I → TCTree) → Sort u} →

{motive_2 : (I : Type 1) × (I → TCTree) → Sort u} →

((a : (I : Prop) × (I → TCTree)) → motive_2 a → motive_1 (TCTree.node a)) →

((a : (I : Type 1) × (I → TCTree)) → motive_2 a → motive_1 (TCTree.node a)) →

((fst : Prop) → (snd : (fun I => I → TCTree) fst) → ((a : fst) → motive_1 (snd a)) → motive_2 ⟨fst, snd⟩) →

((fst : Type 1) → (snd : (fun I => I → TCTree) fst) → ((a : fst) → motive_1 (snd a)) → motive_2 ⟨fst, snd⟩) →

(t : (I : Prop) × (I → TCTree)) → motive_2 t

(t : (I : Type 1) × (I → TCTree)) → motive_2 t

protected def TCTree.ibelow_1 : {motive_1 : TCTree → Prop} →

{motive_2 : (I : Prop) × (I → TCTree) → Prop} → (I : Prop) × (I → TCTree) → Prop :=

{motive_2 : (I : Type 1) × (I → TCTree) → Prop} → (I : Type 1) × (I → TCTree) → Prop :=

fun {motive_1} {motive_2} t =>

TCTree.rec_1 (fun a a_ih => motive_2 a ∧ a_ih)

(fun fst snd snd_ih => (∀ (a : fst), motive_1 (snd a)) ∧ ∀ (a : fst), snd_ih a) t

inductive TCTree : Type

inductive TCTree : Type 2

constructors:

TCTree.node : (I : Prop) × (I → TCTree) → TCTree

TCTree.node : (I : Type 1) × (I → TCTree) → TCTree

def TCTree._sizeOf_inst : SizeOf TCTree :=

{ sizeOf := fun m => m._sizeOf_1 }

theorem TCTree.node.inj : ∀ {a a_1 : (I : Prop) × (I → TCTree)}, TCTree.node a = TCTree.node a_1 → a = a_1 :=

theorem TCTree.node.inj : ∀ {a a_1 : (I : Type 1) × (I → TCTree)}, TCTree.node a = TCTree.node a_1 → a = a_1 :=

fun {a a_1} x => TCTree.noConfusion x fun x => x

def TCTree._sizeOf_1 : TCTree → ℕ :=

fun t => TCTree.rec (fun a a_ih => 1 + a_ih) (fun fst snd snd_ih => 1 + sizeOf fst) t

protected def TCTree.noConfusionType.withCtor.{u} : (P : Type u) →

(ctorIdx : ℕ) → TCTree.noConfusionType.withCtorType P ctorIdx → P → TCTree → P :=

fun P ctorIdx k k' x => x.casesOn fun a => if h : ctorIdx = 0 then (h ▸ k) PUnit.unit a else k'

protected def TCTree.noConfusion.{u} : {P : Sort u} → {x1 x2 : TCTree} → x1 = x2 → TCTree.noConfusionType P x1 x2 :=

fun {P} {x1 x2} h12 =>

Eq.ndrec (motive := fun a => x1 = a → TCTree.noConfusionType P x1 a) (fun h11 => x1.casesOn fun a x => x ⋯) h12 h12

theorem TCTree.node.injEq : ∀ (a a_1 : (I : Prop) × (I → TCTree)), (TCTree.node a = TCTree.node a_1) = (a = a_1) :=

theorem TCTree.node.injEq : ∀ (a a_1 : (I : Type 1) × (I → TCTree)), (TCTree.node a = TCTree.node a_1) = (a = a_1) :=

fun a a_1 =>

Eq.propIntro (fun a_2 => TCTree.noConfusion a_2 fun x => x) fun a_2 =>

Eq.casesOn (motive := fun a_3 x => a_1 = a_3 → a_2 ≍ x → TCTree.node a = TCTree.node a_1) a_2

(fun h =>

Eq.ndrec (motive := fun a_3 => ∀ (a_4 : a = a_3), a_4 ≍ Eq.refl a → TCTree.node a = TCTree.node a_3)

(fun a_3 h => Eq.refl (TCTree.node a)) (Eq.symm h) a_2)

(Eq.refl a_1) (HEq.refl a_2)

protected def TCTree.recOn.{u} : {motive_1 : TCTree → Sort u} →

{motive_2 : (I : Prop) × (I → TCTree) → Sort u} →

{motive_2 : (I : Type 1) × (I → TCTree) → Sort u} →

(t : TCTree) →

((a : (I : Prop) × (I → TCTree)) → motive_2 a → motive_1 (TCTree.node a)) →

((a : (I : Type 1) × (I → TCTree)) → motive_2 a → motive_1 (TCTree.node a)) →

((fst : Prop) → (snd : (fun I => I → TCTree) fst) → ((a : fst) → motive_1 (snd a)) → motive_2 ⟨fst, snd⟩) →

((fst : Type 1) → (snd : (fun I => I → TCTree) fst) → ((a : fst) → motive_1 (snd a)) → motive_2 ⟨fst, snd⟩) →

motive_1 t :=

fun {motive_1} {motive_2} t node mk => TCTree.rec node mk t

protected def TCTree.below_1.{u} : {motive_1 : TCTree → Sort u} →

protected axiom TCTree.below_1.{u} : {motive_1 : TCTree → Sort u} →

{motive_2 : (I : Prop) × (I → TCTree) → Sort u} → (I : Prop) × (I → TCTree) → Sort (max 1 u) :=

{motive_2 : (I : Type 1) × (I → TCTree) → Sort u} → (I : Type 1) × (I → TCTree) → Sort (max 1 u)

fun {motive_1} {motive_2} t =>

TCTree.rec_1 (fun a a_ih => motive_2 a ×' a_ih)

(fun fst snd snd_ih => ((a : fst) → motive_1 (snd a)) ×' ((a : fst) → snd_ih a)) t

protected def TCTree.ibelow : {motive_1 : TCTree → Prop} →

{motive_2 : (I : Prop) × (I → TCTree) → Prop} → TCTree → Prop :=

{motive_2 : (I : Type 1) × (I → TCTree) → Prop} → TCTree → Prop :=

fun {motive_1} {motive_2} t =>

TCTree.rec (fun a a_ih => motive_2 a ∧ a_ih)

(fun fst snd snd_ih => (∀ (a : fst), motive_1 (snd a)) ∧ ∀ (a : fst), snd_ih a) t

recursor TCTree.rec.{u} : {motive_1 : TCTree → Sort u} →

{motive_2 : (I : Prop) × (I → TCTree) → Sort u} →

{motive_2 : (I : Type 1) × (I → TCTree) → Sort u} →

((a : (I : Prop) × (I → TCTree)) → motive_2 a → motive_1 (TCTree.node a)) →

((a : (I : Type 1) × (I → TCTree)) → motive_2 a → motive_1 (TCTree.node a)) →

((fst : Prop) → (snd : (fun I => I → TCTree) fst) → ((a : fst) → motive_1 (snd a)) → motive_2 ⟨fst, snd⟩) →

((fst : Type 1) → (snd : (fun I => I → TCTree) fst) → ((a : fst) → motive_1 (snd a)) → motive_2 ⟨fst, snd⟩) →

(t : TCTree) → motive_1 t

-- Lean.auxRecExt extension: 10 new entries

-- Lean.noConfusionExt extension: 1 new entries

-- Lean.declRangeExt extension: 0 new entries

-- Lean.protectedExt extension: 13 new entries

-- Lean.namespacesExt extension: 3 new entries

-- reducibilityCore extension: 14 new entries

-- Lean.Meta.globalInstanceExtension extension: 1 new entries

-- Lean.Meta.instanceExtension extension: 1 new entries

-- Lean.Meta.simpExtension extension: 2 new entries

-- Lean.Meta.completionBlackListExt extension: 3 new entries

已保存差异

原始文本

打开文件

def TCTree._sizeOf_2 : (I : Prop) × (I → TCTree) → ℕ :=
fun t => TCTree.rec_1 (fun a a_ih => 1 + a_ih) (fun fst snd snd_ih => 1 + sizeOf fst) t

protected def TCTree.noConfusionType.{u} : Sort u → TCTree → TCTree → Sort u :=
fun P x1 x2 => x1.casesOn fun a => TCTree.noConfusionType.withCtor (Sort u) 0 (fun x a_1 => (a = a_1 → P) → P) P x2

protected def TCTree.brecOn.{u} : {motive_1 : TCTree → Sort u} →
  {motive_2 : (I : Prop) × (I → TCTree) → Sort u} →
    (t : TCTree) →
      ((t : TCTree) → t.below → motive_1 t) →
        ((t : (I : Prop) × (I → TCTree)) → TCTree.below_1 t → motive_2 t) → motive_1 t :=
fun {motive_1} {motive_2} t F_1 F_2 =>
  (TCTree.rec (fun a a_ih => ⟨F_1 (TCTree.node a) a_ih, a_ih⟩)
      (fun fst snd snd_ih =>
        ⟨F_2 ⟨fst, snd⟩ ⟨fun a => (snd_ih a).1, fun a => (snd_ih a).2⟩, fun a => (snd_ih a).1, fun a => (snd_ih a).2⟩)
      t).1

protected def TCTree.below.{u} : {motive_1 : TCTree → Sort u} →
  {motive_2 : (I : Prop) × (I → TCTree) → Sort u} → TCTree → Sort (max 1 u) :=
fun {motive_1} {motive_2} t =>
  TCTree.rec (fun a a_ih => motive_2 a ×' a_ih)
    (fun fst snd snd_ih => ((a : fst) → motive_1 (snd a)) ×' ((a : fst) → snd_ih a)) t

protected def TCTree.noConfusionType.withCtorType.{u} : Type u → ℕ → Type (max 1 u) :=
fun P ctorIdx => PUnit.{2} → (I : Prop) × (I → TCTree) → P

constructor TCTree.node : (I : Prop) × (I → TCTree) → TCTree

protected def TCTree.binductionOn_1 : ∀ {motive_1 : TCTree → Prop} {motive_2 : (I : Prop) × (I → TCTree) → Prop}
  (t : (I : Prop) × (I → TCTree)),
  (∀ (t : TCTree), t.ibelow → motive_1 t) →
    (∀ (t : (I : Prop) × (I → TCTree)), TCTree.ibelow_1 t → motive_2 t) → motive_2 t :=
fun {motive_1} {motive_2} t F_1 F_2 =>
  (TCTree.rec_1 (fun a a_ih => ⟨F_1 (TCTree.node a) a_ih, a_ih⟩)
      (fun fst snd snd_ih =>
        ⟨F_2 ⟨fst, snd⟩ ⟨fun a => (snd_ih a).1, fun a => (snd_ih a).2⟩, ⟨fun a => (snd_ih a).1, fun a => (snd_ih a).2⟩⟩)
      t).1

protected def TCTree.brecOn_1.{u} : {motive_1 : TCTree → Sort u} →
  {motive_2 : (I : Prop) × (I → TCTree) → Sort u} →
    (t : (I : Prop) × (I → TCTree)) →
      ((t : TCTree) → t.below → motive_1 t) →
        ((t : (I : Prop) × (I → TCTree)) → TCTree.below_1 t → motive_2 t) → motive_2 t :=
fun {motive_1} {motive_2} t F_1 F_2 =>
  (TCTree.rec_1 (fun a a_ih => ⟨F_1 (TCTree.node a) a_ih, a_ih⟩)
      (fun fst snd snd_ih =>
        ⟨F_2 ⟨fst, snd⟩ ⟨fun a => (snd_ih a).1, fun a => (snd_ih a).2⟩, fun a => (snd_ih a).1, fun a => (snd_ih a).2⟩)
      t).1

protected def TCTree.binductionOn : ∀ {motive_1 : TCTree → Prop} {motive_2 : (I : Prop) × (I → TCTree) → Prop}
  (t : TCTree),
  (∀ (t : TCTree), t.ibelow → motive_1 t) →
    (∀ (t : (I : Prop) × (I → TCTree)), TCTree.ibelow_1 t → motive_2 t) → motive_1 t :=
fun {motive_1} {motive_2} t F_1 F_2 =>
  (TCTree.rec (fun a a_ih => ⟨F_1 (TCTree.node a) a_ih, a_ih⟩)
      (fun fst snd snd_ih =>
        ⟨F_2 ⟨fst, snd⟩ ⟨fun a => (snd_ih a).1, fun a => (snd_ih a).2⟩, ⟨fun a => (snd_ih a).1, fun a => (snd_ih a).2⟩⟩)
      t).1

def TCTree.casesOn.{u} : {motive_1 : TCTree → Sort u} →
  (t : TCTree) → ((a : (I : Prop) × (I → TCTree)) → motive_1 (TCTree.node a)) → motive_1 t :=
fun {motive_1} t node => TCTree.rec (fun a a_ih => node a) (fun fst snd snd_ih => PUnit.unit) t

theorem TCTree.node.sizeOf_spec : ∀ (a : (I : Prop) × (I → TCTree)), sizeOf (TCTree.node a) = 1 + sizeOf a :=
fun a => Eq.refl (1 + sizeOf a)

recursor TCTree.rec_1.{u} : {motive_1 : TCTree → Sort u} →
  {motive_2 : (I : Prop) × (I → TCTree) → Sort u} →
    ((a : (I : Prop) × (I → TCTree)) → motive_2 a → motive_1 (TCTree.node a)) →
      ((fst : Prop) → (snd : (fun I => I → TCTree) fst) → ((a : fst) → motive_1 (snd a)) → motive_2 ⟨fst, snd⟩) →
        (t : (I : Prop) × (I → TCTree)) → motive_2 t

protected def TCTree.ibelow_1 : {motive_1 : TCTree → Prop} →
  {motive_2 : (I : Prop) × (I → TCTree) → Prop} → (I : Prop) × (I → TCTree) → Prop :=
fun {motive_1} {motive_2} t =>
  TCTree.rec_1 (fun a a_ih => motive_2 a ∧ a_ih)
    (fun fst snd snd_ih => (∀ (a : fst), motive_1 (snd a)) ∧ ∀ (a : fst), snd_ih a) t

inductive TCTree : Type
constructors:
TCTree.node : (I : Prop) × (I → TCTree) → TCTree

def TCTree._sizeOf_inst : SizeOf TCTree :=
{ sizeOf := fun m => m._sizeOf_1 }

theorem TCTree.node.inj : ∀ {a a_1 : (I : Prop) × (I → TCTree)}, TCTree.node a = TCTree.node a_1 → a = a_1 :=
fun {a a_1} x => TCTree.noConfusion x fun x => x

def TCTree._sizeOf_1 : TCTree → ℕ :=
fun t => TCTree.rec (fun a a_ih => 1 + a_ih) (fun fst snd snd_ih => 1 + sizeOf fst) t

protected def TCTree.noConfusionType.withCtor.{u} : (P : Type u) →
  (ctorIdx : ℕ) → TCTree.noConfusionType.withCtorType P ctorIdx → P → TCTree → P :=
fun P ctorIdx k k' x => x.casesOn fun a => if h : ctorIdx = 0 then (h ▸ k) PUnit.unit a else k'

protected def TCTree.noConfusion.{u} : {P : Sort u} → {x1 x2 : TCTree} → x1 = x2 → TCTree.noConfusionType P x1 x2 :=
fun {P} {x1 x2} h12 =>
  Eq.ndrec (motive := fun a => x1 = a → TCTree.noConfusionType P x1 a) (fun h11 => x1.casesOn fun a x => x ⋯) h12 h12

theorem TCTree.node.injEq : ∀ (a a_1 : (I : Prop) × (I → TCTree)), (TCTree.node a = TCTree.node a_1) = (a = a_1) :=
fun a a_1 =>
  Eq.propIntro (fun a_2 => TCTree.noConfusion a_2 fun x => x) fun a_2 =>
    Eq.casesOn (motive := fun a_3 x => a_1 = a_3 → a_2 ≍ x → TCTree.node a = TCTree.node a_1) a_2
      (fun h =>
        Eq.ndrec (motive := fun a_3 => ∀ (a_4 : a = a_3), a_4 ≍ Eq.refl a → TCTree.node a = TCTree.node a_3)
          (fun a_3 h => Eq.refl (TCTree.node a)) (Eq.symm h) a_2)
      (Eq.refl a_1) (HEq.refl a_2)

protected def TCTree.recOn.{u} : {motive_1 : TCTree → Sort u} →
  {motive_2 : (I : Prop) × (I → TCTree) → Sort u} →
    (t : TCTree) →
      ((a : (I : Prop) × (I → TCTree)) → motive_2 a → motive_1 (TCTree.node a)) →
        ((fst : Prop) → (snd : (fun I => I → TCTree) fst) → ((a : fst) → motive_1 (snd a)) → motive_2 ⟨fst, snd⟩) →
          motive_1 t :=
fun {motive_1} {motive_2} t node mk => TCTree.rec node mk t

protected def TCTree.below_1.{u} : {motive_1 : TCTree → Sort u} →
  {motive_2 : (I : Prop) × (I → TCTree) → Sort u} → (I : Prop) × (I → TCTree) → Sort (max 1 u) :=
fun {motive_1} {motive_2} t =>
  TCTree.rec_1 (fun a a_ih => motive_2 a ×' a_ih)
    (fun fst snd snd_ih => ((a : fst) → motive_1 (snd a)) ×' ((a : fst) → snd_ih a)) t

protected def TCTree.ibelow : {motive_1 : TCTree → Prop} →
  {motive_2 : (I : Prop) × (I → TCTree) → Prop} → TCTree → Prop :=
fun {motive_1} {motive_2} t =>
  TCTree.rec (fun a a_ih => motive_2 a ∧ a_ih)
    (fun fst snd snd_ih => (∀ (a : fst), motive_1 (snd a)) ∧ ∀ (a : fst), snd_ih a) t

recursor TCTree.rec.{u} : {motive_1 : TCTree → Sort u} →
  {motive_2 : (I : Prop) × (I → TCTree) → Sort u} →
    ((a : (I : Prop) × (I → TCTree)) → motive_2 a → motive_1 (TCTree.node a)) →
      ((fst : Prop) → (snd : (fun I => I → TCTree) fst) → ((a : fst) → motive_1 (snd a)) → motive_2 ⟨fst, snd⟩) →
        (t : TCTree) → motive_1 t

-- Lean.auxRecExt extension: 10 new entries

-- Lean.noConfusionExt extension: 1 new entries

-- Lean.declRangeExt extension: 0 new entries

-- Lean.protectedExt extension: 13 new entries

-- Lean.namespacesExt extension: 3 new entries

-- reducibilityCore extension: 14 new entries

-- Lean.Meta.globalInstanceExtension extension: 1 new entries

-- Lean.Meta.instanceExtension extension: 1 new entries

-- Lean.Meta.simpExtension extension: 2 new entries

-- Lean.Meta.completionBlackListExt extension: 3 new entries

更改后文本

打开文件

def TCTree._sizeOf_2 : (I : Type 1) × (I → TCTree) → ℕ :=
fun t => TCTree.rec_1 (fun a a_ih => 1 + a_ih) (fun fst snd snd_ih => 1 + sizeOf fst) t

protected axiom TCTree.brecOn.{u} : {motive_1 : TCTree → Sort u} →
  {motive_2 : (I : Type 1) × (I → TCTree) → Sort u} →
    (t : TCTree) →
      ((t : TCTree) → t.below → motive_1 t) →
        ((t : (I : Type 1) × (I → TCTree)) → TCTree.below_1 t → motive_2 t) → motive_1 t

protected axiom TCTree.below.{u} : {motive_1 : TCTree → Sort u} →
  {motive_2 : (I : Type 1) × (I → TCTree) → Sort u} → TCTree → Sort (max 1 u)

protected def TCTree.noConfusionType.withCtorType.{u} : Type u → ℕ → Type (max 3 u) :=
fun P ctorIdx => PUnit.{4} → (I : Type 1) × (I → TCTree) → P

constructor TCTree.node : (I : Type 1) × (I → TCTree) → TCTree

protected def TCTree.binductionOn_1 : ∀ {motive_1 : TCTree → Prop} {motive_2 : (I : Type 1) × (I → TCTree) → Prop}
  (t : (I : Type 1) × (I → TCTree)),
  (∀ (t : TCTree), t.ibelow → motive_1 t) →
    (∀ (t : (I : Type 1) × (I → TCTree)), TCTree.ibelow_1 t → motive_2 t) → motive_2 t :=
fun {motive_1} {motive_2} t F_1 F_2 =>
  (TCTree.rec_1 (fun a a_ih => ⟨F_1 (TCTree.node a) a_ih, a_ih⟩)
      (fun fst snd snd_ih =>
        ⟨F_2 ⟨fst, snd⟩ ⟨fun a => (snd_ih a).1, fun a => (snd_ih a).2⟩, ⟨fun a => (snd_ih a).1, fun a => (snd_ih a).2⟩⟩)
      t).1

protected axiom TCTree.brecOn_1.{u} : {motive_1 : TCTree → Sort u} →
  {motive_2 : (I : Type 1) × (I → TCTree) → Sort u} →
    (t : (I : Type 1) × (I → TCTree)) →
      ((t : TCTree) → t.below → motive_1 t) →
        ((t : (I : Type 1) × (I → TCTree)) → TCTree.below_1 t → motive_2 t) → motive_2 t

protected def TCTree.binductionOn : ∀ {motive_1 : TCTree → Prop} {motive_2 : (I : Type 1) × (I → TCTree) → Prop}
  (t : TCTree),
  (∀ (t : TCTree), t.ibelow → motive_1 t) →
    (∀ (t : (I : Type 1) × (I → TCTree)), TCTree.ibelow_1 t → motive_2 t) → motive_1 t :=
fun {motive_1} {motive_2} t F_1 F_2 =>
  (TCTree.rec (fun a a_ih => ⟨F_1 (TCTree.node a) a_ih, a_ih⟩)
      (fun fst snd snd_ih =>
        ⟨F_2 ⟨fst, snd⟩ ⟨fun a => (snd_ih a).1, fun a => (snd_ih a).2⟩, ⟨fun a => (snd_ih a).1, fun a => (snd_ih a).2⟩⟩)
      t).1

def TCTree.casesOn.{u} : {motive_1 : TCTree → Sort u} →
  (t : TCTree) → ((a : (I : Type 1) × (I → TCTree)) → motive_1 (TCTree.node a)) → motive_1 t :=
fun {motive_1} t node => TCTree.rec (fun a a_ih => node a) (fun fst snd snd_ih => PUnit.unit) t

theorem TCTree.node.sizeOf_spec : ∀ (a : (I : Type 1) × (I → TCTree)), sizeOf (TCTree.node a) = 1 + sizeOf a :=
fun a => Eq.refl (1 + sizeOf a)

recursor TCTree.rec_1.{u} : {motive_1 : TCTree → Sort u} →
  {motive_2 : (I : Type 1) × (I → TCTree) → Sort u} →
    ((a : (I : Type 1) × (I → TCTree)) → motive_2 a → motive_1 (TCTree.node a)) →
      ((fst : Type 1) → (snd : (fun I => I → TCTree) fst) → ((a : fst) → motive_1 (snd a)) → motive_2 ⟨fst, snd⟩) →
        (t : (I : Type 1) × (I → TCTree)) → motive_2 t

protected def TCTree.ibelow_1 : {motive_1 : TCTree → Prop} →
  {motive_2 : (I : Type 1) × (I → TCTree) → Prop} → (I : Type 1) × (I → TCTree) → Prop :=
fun {motive_1} {motive_2} t =>
  TCTree.rec_1 (fun a a_ih => motive_2 a ∧ a_ih)
    (fun fst snd snd_ih => (∀ (a : fst), motive_1 (snd a)) ∧ ∀ (a : fst), snd_ih a) t

inductive TCTree : Type 2
constructors:
TCTree.node : (I : Type 1) × (I → TCTree) → TCTree

def TCTree._sizeOf_inst : SizeOf TCTree :=
{ sizeOf := fun m => m._sizeOf_1 }

theorem TCTree.node.inj : ∀ {a a_1 : (I : Type 1) × (I → TCTree)}, TCTree.node a = TCTree.node a_1 → a = a_1 :=
fun {a a_1} x => TCTree.noConfusion x fun x => x

def TCTree._sizeOf_1 : TCTree → ℕ :=
fun t => TCTree.rec (fun a a_ih => 1 + a_ih) (fun fst snd snd_ih => 1 + sizeOf fst) t

theorem TCTree.node.injEq : ∀ (a a_1 : (I : Type 1) × (I → TCTree)), (TCTree.node a = TCTree.node a_1) = (a = a_1) :=
fun a a_1 =>
  Eq.propIntro (fun a_2 => TCTree.noConfusion a_2 fun x => x) fun a_2 =>
    Eq.casesOn (motive := fun a_3 x => a_1 = a_3 → a_2 ≍ x → TCTree.node a = TCTree.node a_1) a_2
      (fun h =>
        Eq.ndrec (motive := fun a_3 => ∀ (a_4 : a = a_3), a_4 ≍ Eq.refl a → TCTree.node a = TCTree.node a_3)
          (fun a_3 h => Eq.refl (TCTree.node a)) (Eq.symm h) a_2)
      (Eq.refl a_1) (HEq.refl a_2)

protected def TCTree.recOn.{u} : {motive_1 : TCTree → Sort u} →
  {motive_2 : (I : Type 1) × (I → TCTree) → Sort u} →
    (t : TCTree) →
      ((a : (I : Type 1) × (I → TCTree)) → motive_2 a → motive_1 (TCTree.node a)) →
        ((fst : Type 1) → (snd : (fun I => I → TCTree) fst) → ((a : fst) → motive_1 (snd a)) → motive_2 ⟨fst, snd⟩) →
          motive_1 t :=
fun {motive_1} {motive_2} t node mk => TCTree.rec node mk t

protected axiom TCTree.below_1.{u} : {motive_1 : TCTree → Sort u} →
  {motive_2 : (I : Type 1) × (I → TCTree) → Sort u} → (I : Type 1) × (I → TCTree) → Sort (max 1 u)

protected def TCTree.ibelow : {motive_1 : TCTree → Prop} →
  {motive_2 : (I : Type 1) × (I → TCTree) → Prop} → TCTree → Prop :=
fun {motive_1} {motive_2} t =>
  TCTree.rec (fun a a_ih => motive_2 a ∧ a_ih)
    (fun fst snd snd_ih => (∀ (a : fst), motive_1 (snd a)) ∧ ∀ (a : fst), snd_ih a) t

recursor TCTree.rec.{u} : {motive_1 : TCTree → Sort u} →
  {motive_2 : (I : Type 1) × (I → TCTree) → Sort u} →
    ((a : (I : Type 1) × (I → TCTree)) → motive_2 a → motive_1 (TCTree.node a)) →
      ((fst : Type 1) → (snd : (fun I => I → TCTree) fst) → ((a : fst) → motive_1 (snd a)) → motive_2 ⟨fst, snd⟩) →
        (t : TCTree) → motive_1 t

-- Lean.auxRecExt extension: 10 new entries

-- Lean.noConfusionExt extension: 1 new entries

-- Lean.declRangeExt extension: 0 new entries

-- Lean.protectedExt extension: 13 new entries

-- Lean.namespacesExt extension: 3 new entries

-- reducibilityCore extension: 14 new entries

-- Lean.Meta.globalInstanceExtension extension: 1 new entries

-- Lean.Meta.instanceExtension extension: 1 new entries

-- Lean.Meta.simpExtension extension: 2 new entries

-- Lean.Meta.completionBlackListExt extension: 3 new entries