Primitive Recursive Functions in $\mathsf{I} \Sigma_1$ #
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
Equations
- p.resultDeltaDef = LO.FirstOrder.Arith.HierarchySymbol.Semiformula.graphDelta p.resultDef
Instances For
structure
LO.Arith.PR.Construction
(V : Type u_1)
[LO.ORingStruc V]
{k : β}
(p : LO.Arith.PR.Blueprint k)
:
Type u_1
- zero : (Fin k β V) β V
- succ : (Fin k β V) β V β V β V
- zero_defined : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction self.zero p.zero
- succ_defined : LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction (fun (v : Fin k.succ.succ β V) => self.succ (fun (x : Fin k) => v x.succ.succ) (v 1) (v 0)) p.succ
Instances For
theorem
LO.Arith.PR.Construction.zero_defined
{V : Type u_1}
[LO.ORingStruc V]
{k : β}
{p : LO.Arith.PR.Blueprint k}
(self : LO.Arith.PR.Construction V p)
:
LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction self.zero p.zero
theorem
LO.Arith.PR.Construction.succ_defined
{V : Type u_1}
[LO.ORingStruc V]
{k : β}
{p : LO.Arith.PR.Blueprint k}
(self : LO.Arith.PR.Construction V p)
:
LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction
(fun (v : Fin k.succ.succ β V) => self.succ (fun (x : Fin k) => v x.succ.succ) (v 1) (v 0)) p.succ
def
LO.Arith.PR.Construction.CSeq
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{k : β}
{p : LO.Arith.PR.Blueprint k}
(c : LO.Arith.PR.Construction V p)
(v : Fin k β V)
(s : V)
:
Equations
- c.CSeq v s = (LO.Arith.Seq s β§ βͺ0, c.zero vβ« β s β§ β i < LO.Arith.lh s - 1, β (z : V), βͺi, zβ« β s β βͺi + 1, c.succ v i zβ« β s)
Instances For
theorem
LO.Arith.PR.Construction.cseq_defined
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{k : β}
{p : LO.Arith.PR.Blueprint k}
(c : LO.Arith.PR.Construction V p)
:
LO.FirstOrder.Arith.HierarchySymbol.Defined (fun (v : Fin (k + 1) β V) => c.CSeq (fun (x : Fin k) => v x.succ) (v 0))
p.cseqDef
@[simp]
theorem
LO.Arith.PR.Construction.cseq_defined_iff
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{k : β}
{p : LO.Arith.PR.Blueprint k}
(c : LO.Arith.PR.Construction V p)
(v : Fin (k + 1) β V)
:
V β§/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val p.cseqDef) β c.CSeq (fun (x : Fin k) => v x.succ) (v 0)
theorem
LO.Arith.PR.Construction.CSeq.seq
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{k : β}
{p : LO.Arith.PR.Blueprint k}
{c : LO.Arith.PR.Construction V p}
{v : Fin k β V}
{s : V}
(h : c.CSeq v s)
:
theorem
LO.Arith.PR.Construction.CSeq.zero
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{k : β}
{p : LO.Arith.PR.Blueprint k}
{c : LO.Arith.PR.Construction V p}
{v : Fin k β V}
{s : V}
(h : c.CSeq v s)
:
βͺ0, c.zero vβ« β s
theorem
LO.Arith.PR.Construction.CSeq.succ
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{k : β}
{p : LO.Arith.PR.Blueprint k}
{c : LO.Arith.PR.Construction V p}
{v : Fin k β V}
{s : V}
(h : c.CSeq v s)
(i : V)
:
theorem
LO.Arith.PR.Construction.CSeq.unique
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{k : β}
{p : LO.Arith.PR.Blueprint k}
{c : LO.Arith.PR.Construction V p}
{v : Fin k β V}
{sβ : V}
{sβ : V}
(Hβ : c.CSeq v sβ)
(Hβ : c.CSeq v sβ)
(hββ : LO.Arith.lh sβ β€ LO.Arith.lh sβ)
{i : V}
(hi : i < LO.Arith.lh sβ)
{zβ : V}
{zβ : V}
:
theorem
LO.Arith.PR.Construction.CSeq.initial
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{k : β}
{p : LO.Arith.PR.Blueprint k}
{c : LO.Arith.PR.Construction V p}
{v : Fin k β V}
:
c.CSeq v !β¦c.zero vβ§
theorem
LO.Arith.PR.Construction.CSeq.successor
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{k : β}
{p : LO.Arith.PR.Blueprint k}
{c : LO.Arith.PR.Construction V p}
{v : Fin k β V}
{s : V}
{l : V}
{z : V}
(Hs : c.CSeq v s)
(hl : l + 1 = LO.Arith.lh s)
(hz : βͺl, zβ« β s)
:
c.CSeq v (s β' c.succ v l z)
theorem
LO.Arith.PR.Construction.CSeq.exists
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{k : β}
{p : LO.Arith.PR.Blueprint k}
(c : LO.Arith.PR.Construction V p)
(v : Fin k β V)
(l : V)
:
β (s : V), c.CSeq v s β§ l + 1 = LO.Arith.lh s
theorem
LO.Arith.PR.Construction.cSeq_result_existsUnique
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{k : β}
{p : LO.Arith.PR.Blueprint k}
(c : LO.Arith.PR.Construction V p)
(v : Fin k β V)
(l : V)
:
def
LO.Arith.PR.Construction.result
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{k : β}
{p : LO.Arith.PR.Blueprint k}
(c : LO.Arith.PR.Construction V p)
(v : Fin k β V)
(u : V)
:
V
Equations
- c.result v u = Classical.choose! β―
Instances For
theorem
LO.Arith.PR.Construction.result_spec
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{k : β}
{p : LO.Arith.PR.Blueprint k}
(c : LO.Arith.PR.Construction V p)
(v : Fin k β V)
(u : V)
:
@[simp]
theorem
LO.Arith.PR.Construction.result_zero
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{k : β}
{p : LO.Arith.PR.Blueprint k}
(c : LO.Arith.PR.Construction V p)
(v : Fin k β V)
:
c.result v 0 = c.zero v
@[simp]
theorem
LO.Arith.PR.Construction.result_succ
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{k : β}
{p : LO.Arith.PR.Blueprint k}
(c : LO.Arith.PR.Construction V p)
(v : Fin k β V)
(u : V)
:
theorem
LO.Arith.PR.Construction.result_graph
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{k : β}
{p : LO.Arith.PR.Blueprint k}
(c : LO.Arith.PR.Construction V p)
(v : Fin k β V)
(z : V)
(u : V)
:
theorem
LO.Arith.PR.Construction.result_defined
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{k : β}
{p : LO.Arith.PR.Blueprint k}
(c : LO.Arith.PR.Construction V p)
:
LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction
(fun (v : Fin (k + 1) β V) => c.result (fun (x : Fin k) => v x.succ) (v 0)) p.resultDef
theorem
LO.Arith.PR.Construction.result_defined_delta
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{k : β}
{p : LO.Arith.PR.Blueprint k}
(c : LO.Arith.PR.Construction V p)
:
LO.FirstOrder.Arith.HierarchySymbol.DefinedFunction
(fun (v : Fin (k + 1) β V) => c.result (fun (x : Fin k) => v x.succ) (v 0)) p.resultDeltaDef
@[simp]
theorem
LO.Arith.PR.Construction.result_defined_iff
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{k : β}
{p : LO.Arith.PR.Blueprint k}
(c : LO.Arith.PR.Construction V p)
(v : Fin (k + 2) β V)
:
V β§/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val p.resultDef) β v 0 = c.result (fun (x : Fin k) => v x.succ.succ) (v 1)
instance
LO.Arith.PR.Construction.result_definable
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{k : β}
{p : LO.Arith.PR.Blueprint k}
(c : LO.Arith.PR.Construction V p)
:
Equations
- β― = β―
instance
LO.Arith.PR.Construction.result_definable_deltaβ
{V : Type u_1}
[LO.ORingStruc V]
[V β§β* ππΊβ]
{k : β}
{p : LO.Arith.PR.Blueprint k}
(c : LO.Arith.PR.Construction V p)
:
Equations
- β― = β―