Compare text

Find the difference between two text files

Real-time editor

Hide unchanged lines

Disable line wrap

Layout

Diff precision

Syntax highlighting

Diffchecker Desktop The most secure way to run Diffchecker. Get the Diffchecker Desktop app: your diffs never leave your computer!Get Desktop

TCTree

Created last yearDiff never expires

60 removals

Lines
Total
Removed

Characters
Total
Removed

To continue using this feature, upgrade to Diffchecker Pro View Pricing

153 lines

41 additions

Lines
Total
Added

Characters
Total
Added

To continue using this feature, upgrade to Diffchecker Pro View Pricing

137 lines

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

Saved diffs

Original text

Open file

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

Changed text

Open file

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