Comparar texto

Encontre a diferença entre dois arquivos de texto

Editor live

Recolher inalteradas

Sem quebra de linha

Layout

Nível de detalhe

Realce de sintaxe

Diffchecker Desktop A maneira mais segura de usar o Diffchecker. Obtenha o aplicativo Diffchecker Desktop: seus diffs nunca saem do seu computador!Obter Desktop

TCTree

Criado ano passadoO diff nunca expira

60 remoções

Linhas
Total
Removido

Caracteres
Total
Removido

Para continuar usando este recurso, atualize para Diffchecker Pro Ver preços

153 linhas

41 adições

Linhas
Total
Adicionado

Caracteres
Total
Adicionado

Para continuar usando este recurso, atualize para Diffchecker Pro Ver preços

137 linhas

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

Diferenças salvas

Texto original

Abrir arquivo

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 alterado

Abrir arquivo

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