Texte vergleichen

Finde den Unterschied zwischen zwei Textdateien

Live-Editor

Gleiches ausblenden

Zeilenumbruch aus

Ansicht

Vergleichsgenauigkeit

Syntaxhervorhebung

Diffchecker Desktop Der sicherste Weg, Diffchecker zu nutzen. Hol dir die Desktop-App: Deine Diffs verlassen nie deinen Computer!Desktop holen

TCTree

Erstellt letztes JahrDiff läuft nie ab

60 Entfernungen

Zeilen
Gesamt
Entfernt

Zeichen
Gesamt
Entfernt

Um diese Funktion weiterhin zu nutzen, aktualisiere auf Diffchecker Pro Preise anzeigen

153 Zeilen

41 Hinzufügungen

Zeilen
Gesamt
Hinzugefügt

Zeichen
Gesamt
Hinzugefügt

Um diese Funktion weiterhin zu nutzen, aktualisiere auf Diffchecker Pro Preise anzeigen

137 Zeilen

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

Gespeicherte Diffs

Originaltext

Datei öffnen

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

Bearbeitung

Datei öffnen

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