Documentation

Arithmetization.ISigmaOne.HFS.Fixpoint

Fixpoint Construction #

Instances For
    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.
    Instances For
      Equations
      • φ.limSeqDef = φ.prBlueprint.resultDef
      Instances For
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Instances For
              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
              • finite : ∀ {C : Set V} {v : Fin kV} {x : V}, c v C x∃ (m : V), c v {y : V | y C y < m} x
              Instances
                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
                • strong_finite : ∀ {C : Set V} {v : Fin kV} {x : V}, c v C xc v {y : V | y C y < x} x
                Instances
                  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
                  Instances For
                    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 := }
                    Instances For
                      Equations
                      • c.limSeq v s = c.prConstruction.result v s
                      Instances For
                        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
                        Instances For
                          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