Comparar texto

Encuentra la diferencia entre dos archivos de texto

Editor live

Ocultar sin cambios

Sin ajuste de línea

Vista

Nivel de detalle

Resaltado de sintaxis

Diffchecker Desktop La forma más segura de usar Diffchecker. ¡Obtén la app de Diffchecker Desktop: tus diffs nunca salen de tu computadora!Obtener Desktop

TCTree

Creado el año pasadoEl diff nunca expira

60 eliminaciones

Líneas
Total
Eliminado

Caracteres
Total
Eliminado

Para continuar usando esta función, actualice a Diffchecker Pro Ver precios

153 líneas

41 adiciones

Líneas
Total
Añadido

Caracteres
Total
Añadido

Para continuar usando esta función, actualice a Diffchecker Pro Ver precios

137 líneas

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

Diferencias guardadas

Texto original

Abrir archivo

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

Texto modificado

Abrir archivo

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