Documentation

Arithmetization.ISigmaOne.HFS.Fixpoint

Fixpoint Construction #

Equations
  • LO.Arith.Fixpoint.Blueprint.instCoeSemisentenceDeltaOneHAddNatOfNat = { coe := LO.Arith.Fixpoint.Blueprint.core }
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • φ.limSeqDef = φ.prBlueprint.resultDef
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
theorem LO.Arith.Fixpoint.Construction.defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } {φ : LO.Arith.Fixpoint.Blueprint k} (self : LO.Arith.Fixpoint.Construction V φ) :
LO.FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin k.succ.succV) => self (fun (x : Fin k) => v x.succ.succ) {x : V | x v 1} (v 0)) φ.core
theorem LO.Arith.Fixpoint.Construction.monotone {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } {φ : LO.Arith.Fixpoint.Blueprint k} (self : LO.Arith.Fixpoint.Construction V φ) {C : Set V} {C' : Set V} (h : C C') {v : Fin kV} {x : V} :
self v C xself v C' x
theorem LO.Arith.Fixpoint.Construction.Finite.finite {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } {φ : LO.Arith.Fixpoint.Blueprint k} {c : LO.Arith.Fixpoint.Construction V φ} [self : LO.Arith.Fixpoint.Construction.Finite V c] {C : Set V} {v : Fin kV} {x : V} :
c v C x∃ (m : V), c v {y : V | y C y < m} x
theorem LO.Arith.Fixpoint.Construction.StrongFinite.strong_finite {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } {φ : LO.Arith.Fixpoint.Blueprint k} {c : LO.Arith.Fixpoint.Construction V φ} [self : LO.Arith.Fixpoint.Construction.StrongFinite V c] {C : Set V} {v : Fin kV} {x : V} :
c v C xc v {y : V | y C y < x} x
theorem LO.Arith.Fixpoint.Construction.eval_formula {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) (v : Fin k.succ.succV) :
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val φ.core) c (fun (x : Fin k) => v x.succ.succ) {x : V | x v 1} (v 0)
theorem LO.Arith.Fixpoint.Construction.succ_existsUnique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) (v : Fin kV) (s : V) (ih : V) :
∃! u : V, ∀ (x : V), x u x s c v {z : V | z ih} x
def LO.Arith.Fixpoint.Construction.succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) (v : Fin kV) (s : V) (ih : V) :
V
Equations
theorem LO.Arith.Fixpoint.Construction.mem_succ_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) {x : V} {v : Fin kV} {s : V} {ih : V} :
x c.succ v s ih x s c v {z : V | z ih} x
theorem LO.Arith.Fixpoint.Construction.succ_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) :
LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin (k + 2)V) => c.succ (fun (x : Fin k) => v x.succ.succ) (v 1) (v 0)) φ.succDef
theorem LO.Arith.Fixpoint.Construction.eval_succDef {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) (v : Fin (k + 3)V) :
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val φ.succDef) v 0 = c.succ (fun (x : Fin k) => v x.succ.succ.succ) (v 2) (v 1)
Equations
  • c.prConstruction = { zero := fun (x : Fin kV) => , succ := c.succ, zero_defined := , succ_defined := }
Equations
  • c.limSeq v s = c.prConstruction.result v s
theorem LO.Arith.Fixpoint.Construction.limSeq_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) {v : Fin kV} (s : V) :
c.limSeq v (s + 1) = c.succ v s (c.limSeq v s)
theorem LO.Arith.Fixpoint.Construction.termSet_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) :
LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin k.succV) => c.limSeq (fun (x : Fin k) => v x.succ) (v 0)) φ.limSeqDef
@[simp]
theorem LO.Arith.Fixpoint.Construction.eval_limSeqDef {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) (v : Fin (k + 2)V) :
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val φ.limSeqDef) v 0 = c.limSeq (fun (x : Fin k) => v x.succ.succ) (v 1)
instance LO.Arith.Fixpoint.Construction.limSeq_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) :
𝚺₁.BoldfaceFunction fun (v : Fin k.succV) => c.limSeq (fun (x : Fin k) => v x.succ) (v 0)
Equations
  • =
@[simp]
instance LO.Arith.Fixpoint.Construction.limSeq_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) {m : } (Γ : LO.SigmaPiDelta) :
{ Γ := Γ, rank := m + 1 }.BoldfaceFunction fun (v : Fin k.succV) => c.limSeq (fun (x : Fin k) => v x.succ) (v 0)
Equations
  • =
theorem LO.Arith.Fixpoint.Construction.mem_limSeq_succ_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) {v : Fin kV} {x : V} {s : V} :
x c.limSeq v (s + 1) x s c v {z : V | z c.limSeq v s} x
theorem LO.Arith.Fixpoint.Construction.limSeq_cumulative {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) {v : Fin kV} {s : V} {s' : V} :
s s'c.limSeq v s c.limSeq v s'
theorem LO.Arith.Fixpoint.Construction.mem_limSeq_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) {v : Fin kV} [LO.Arith.Fixpoint.Construction.StrongFinite V c] {u : V} {s : V} :
u c.limSeq v su c.limSeq v (u + 1)
Equations
  • c.Fixpoint v x = ∃ (s : V), x c.limSeq v s
theorem LO.Arith.Fixpoint.Construction.fixpoint_iff_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) {v : Fin kV} {x : V} :
c.Fixpoint v x ∃ (u : V), x c.limSeq v (u + 1)
theorem LO.Arith.Fixpoint.Construction.finite_upperbound {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) {v : Fin kV} (m : V) :
∃ (s : V), z < m, c.Fixpoint v zz c.limSeq v s
theorem LO.Arith.Fixpoint.Construction.case {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) {v : Fin kV} {x : V} [LO.Arith.Fixpoint.Construction.Finite V c] :
c.Fixpoint v x c v {z : V | c.Fixpoint v z} x
theorem LO.Arith.Fixpoint.Construction.fixpoint_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) :
LO.FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin k.succV) => c.Fixpoint (fun (x : Fin k) => v x.succ) (v 0)) φ.fixpointDef
@[simp]
theorem LO.Arith.Fixpoint.Construction.eval_fixpointDef {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) (v : Fin (k + 1)V) :
V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val φ.fixpointDef) c.Fixpoint (fun (x : Fin k) => v x.succ) (v 0)
theorem LO.Arith.Fixpoint.Construction.induction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {k : } {φ : LO.Arith.Fixpoint.Blueprint k} (c : LO.Arith.Fixpoint.Construction V φ) {v : Fin kV} {Γ : LO.SigmaPiDelta} [LO.Arith.Fixpoint.Construction.StrongFinite V c] {P : VProp} (hP : { Γ := Γ, rank := 1 }-Predicate P) (H : ∀ (C : Set V), (xC, c.Fixpoint v x P x)∀ (x : V), c v C xP x) (x : V) :
c.Fixpoint v xP x