# List of theorems

List of theorems in peano_new/arithmetic/naturals/recursion_min.gh:

## Godel's Beta Function

df-beta-just # <summary> A development of <a href="http://en.wikipedia.org/wiki/Kurt_G%C3%B6del">Godel's</a> Beta Function, following Shoenfield(1967). </summary>
(= (min ({|} x (| (+ (* (+ (<,> B x) (1)) (tail A)) (1)) (head A)))) (min ({|} x' (| (+ (* (+ (<,> B x') (1)) (tail A)) (1)) (head A)))))
df-beta # <summary> A development of <a href="http://en.wikipedia.org/wiki/Kurt_G%C3%B6del">Godel's</a> Beta Function, following Shoenfield(1967). </summary>
(= (beta A B) (min ({|} x (| (+ (* (+ (<,> B x) (1)) (tail A)) (1)) (head A)))))
maxex.1 number 116.1
(-> (= x' A) (<-> (-> (fun S) (E. x (A. y (-> (/\ (< (head y) x') (e. y S)) (<= (tail y) x))))) (-> (fun S) (E. x (A. y (-> (/\ (< (head y) A) (e. y S)) (<= (tail y) x)))))))
fun1 number 116.15
(-> (fun S) (E. x (A. y (-> (/\ (= (head y) A) (e. y S)) (= y x)))))
ImpReplaceEx1 # <title> Substitution </title> # <table> # (E. x [ ph ] ] ] ) # (-> [ ph ] [ ps ] ) # (E. x [ [ [ ps ] ) # </table>
(E. x ph) , (-> ph ps)(E. x ps)
ImpReplaceEx1An0 # <title> Substitution </title> # <table> # (E. x (/\ [ ph ] ] ] ch)) # (-> [ ph ] [ ps ] ) # (E. x (/\ [ [ [ ps ] ch)) # </table>
(E. x (/\ ph ch)) , (-> ph ps)(E. x (/\ ps ch))
ImpReplaceEx1An1 # <title> Substitution </title> # <table> # (E. x (/\ ph [ ps ] ] ] )) # (-> [ ps ] [ ch ] ) # (E. x (/\ ph [ [ [ ch ] )) # </table>
(E. x (/\ ph ps)) , (-> ps ch)(E. x (/\ ph ch))
BiReplaceEx1Imp1 # <title> Substitution </title> # <table> # (E. x (-> ph [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (E. x (-> ph [ [ [ ch ] )) # </table>
(E. x (-> ph ps)) , (<-> ps ch)(E. x (-> ph ch))
BiReplaceEx1Imp1An0 # <title> Substitution </title> # <table> # (E. x (-> ph (/\ [ ps ] ] ] th))) # (<-> [ ps ] [ ch ] ) # (E. x (-> ph (/\ [ [ [ ch ] th))) # </table>
(E. x (-> ph (/\ ps th))) , (<-> ps ch)(E. x (-> ph (/\ ch th)))
BiReplaceEx1Imp1An1 # <title> Substitution </title> # <table> # (E. x (-> ph (/\ ps [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (E. x (-> ph (/\ ps [ [ [ th ] ))) # </table>
(E. x (-> ph (/\ ps ch))) , (<-> ch th)(E. x (-> ph (/\ ps th)))
ImpReplaceEx1Imp1 # <title> Substitution </title> # <table> # (E. x (-> ph [ ps ] ] ] )) # (-> [ ps ] [ ch ] ) # (E. x (-> ph [ [ [ ch ] )) # </table>
(E. x (-> ph ps)) , (-> ps ch)(E. x (-> ph ch))
fun1.1 # <summary> Similiar to singleQualifier, but applied to fun1. </summary>
(fun S)(-> (/\ (/\ (= (head B) A) (e. B S)) (/\ (= (head C) A) (e. C S))) (= B C))
(-> (-> (fun S) (E. x (A. y (-> (/\ (< (head y) z) (e. y S)) (<= (tail y) x))))) (-> (fun S) (E. x (A. y (-> (/\ (< (head y) (+ z (1))) (e. y S)) (<= (tail y) x))))))
(-> (fun S) (E. x (A. y (-> (/\ (< (head y) A) (e. y S)) (<= (tail y) x)))))
betaeq1 Equality theorem for beta, first argument
(-> (= A B) (= (beta A C) (beta B C)))
betaeq2 Equality theorem for beta, second argument
(-> (= A B) (= (beta C A) (beta C B)))
(<-> (A. x (-> (| B (* A x)) (| B x))) (A. x' (-> (| B (* A x')) (| B x'))))
df-relprim Definition of "relatively prime"
(<-> (relprim A B) (A. x (-> (| B (* A x)) (| B x))))
relprimex.1 number 120.0 Induction tool for relprimex
(-> (= x' C) (<-> (-> (A. x (A. y (-> (/\ (e. x S) (e. y T)) (relprim x y)))) (E. z (/\ (A. y (-> (/\ (< (+ y (2)) x') (e. (+ y (2)) S)) (| (+ y (2)) z))) (A. y (-> (e. (+ y (2)) T) (-. (| (+ y (2)) z))))))) (-> (A. x (A. y (-> (/\ (e. x S) (e. y T)) (relprim x y)))) (E. z (/\ (A. y (-> (/\ (< (+ y (2)) C) (e. (+ y (2)) S)) (| (+ y (2)) z))) (A. y (-> (e. (+ y (2)) T) (-. (| (+ y (2)) z)))))))))
jctilb number 43.0 jctil with hyps listed backwards
ch , (-> ph ps)(-> ph (/\ ch ps))
relprimex.2 number 122.0 base case for relprimex
(-> (A. x (A. y (-> (/\ (e. x S) (e. y T)) (relprim x y)))) (E. z (/\ (A. y (-> (/\ (< (+ y (2)) (0)) (e. (+ y (2)) S)) (| (+ y (2)) z))) (A. y (-> (e. (+ y (2)) T) (-. (| (+ y (2)) z)))))))
relprimeq2 Equality theorem for relative primeness, second argument
(-> (= A B) (<-> (relprim C A) (relprim C B)))
relprimeq1 Equality theorem for relative primeness, first argument
(-> (= A B) (<-> (relprim A C) (relprim B C)))
(= A B)(<-> (relprim A C) (relprim B C))
(-> ph (= A B))(-> ph (<-> (relprim A C) (relprim B C)))
(= A B)(<-> (relprim C A) (relprim C B))
relprimeq12 # <title> Equivalence for relprim </title> ##
(-> (/\ (= A B) (= C D)) (<-> (relprim A C) (relprim B D)))
(-> ph (= A B))(-> ph (<-> (relprim C A) (relprim C B)))
(-> ph (= A B)) , (-> ph (= C D))(-> ph (<-> (relprim A C) (relprim B D)))
relprimex.3 induction step for relprimex
(-> (-> (A. x (A. y (-> (/\ (e. x S) (e. y T)) (relprim x y)))) (E. z (/\ (A. y (-> (/\ (< (+ y (2)) A) (e. (+ y (2)) S)) (| (+ y (2)) z))) (A. y (-> (e. (+ y (2)) T) (-. (| (+ y (2)) z))))))) (-> (A. x (A. y (-> (/\ (e. x S) (e. y T)) (relprim x y)))) (E. z (/\ (A. y (-> (/\ (< (+ y (2)) (+ A (1))) (e. (+ y (2)) S)) (| (+ y (2)) z))) (A. y (-> (e. (+ y (2)) T) (-. (| (+ y (2)) z))))))))
relprimex number 127.0 # <summary> # A development of Godel's Beta Function, following Shoenfield(1967). # Suppose everything in S is relatively prime to everything in T. # Then there's a number x divisible by everything in (1,A) & S and by nothing in (1, B) & T. # We prove this by induction on A. # </summary>
(-> (A. x (A. y (-> (/\ (e. x S) (e. y T)) (relprim x y)))) (E. z (/\ (A. y (-> (/\ (< (+ y (2)) A) (e. (+ y (2)) S)) (| (+ y (2)) z))) (A. y (-> (e. (+ y (2)) T) (-. (| (+ y (2)) z)))))))
(-> (= (* (+ A (1)) B) (* (+ A (1)) C)) (= B C))
relprimcom number 128.0
(-> (relprim A (+ B (1))) (relprim (+ B (1)) A))
beta.1.1 number 128.5
(relprim (+ A (1)) (+ (* B (+ A (1))) (1)))
beta.1 number 129.0 # <summary> A development of Godel's Beta Function, following Shoenfield(1967). k=A', z=B', j=C </summary>
(-> (| (+ A (1)) (+ B (1))) (relprim (+ (* (+ C (+ A (1))) (+ B (1))) (1)) (+ (* C (+ B (1))) (1))))
BiReplaceBi0Ex1 # <title> Substitution </title> # <table> # (<-> (E. x [ ph ] ] ] ) ch) # (<-> [ ph ] [ ps ] ) # (<-> (E. x [ [ [ ps ] ) ch) # </table>
(<-> (E. x ph) ch) , (<-> ph ps)(<-> (E. x ps) ch)
EqReplaceBi0Ex1Eq0 # <title> Substitution </title> # <table> # (<-> (E. x (= [ A ] ] ] C)) ph) # (= [ A ] [ B ] ) # (<-> (E. x (= [ [ [ B ] C)) ph) # </table>
(<-> (E. x (= A C)) ph) , (= A B)(<-> (E. x (= B C)) ph)
1plus1 # <title> One-digit Addition </title>
(= (+ (1) (1)) (2))
sucsuc number 131.0
(<-> (E. x (= A (+ x (2)))) (< (1) A))
relprimex2 number 133.0 # <summary> Like relprimex, but without the class abstraction </summary>
(rwff x ph) , (rwff v ps)(-> (A. x (A. v (-> (/\ ph ps) (relprim x v)))) (E. z (/\ (A. x (-> (/\ (< (1) x) (/\ (< x A) ph)) (| x z))) (A. v (-> (/\ (< (1) v) ps) (-. (| v z)))))))
exfactorial.1 number 47.0 Induction tool for exfactorial
(-> (= z A) (<-> (E. x (A. y (-> (<= (+ y (1)) (+ z (1))) (| (+ y (1)) (+ x (2)))))) (E. x (A. y (-> (<= (+ y (1)) (+ A (1))) (| (+ y (1)) (+ x (2))))))))
exfactoriallem1 number 47.0 Induction tool for exfactorial
(-> (= z A) (<-> (E. x (A. y (-> (<= (+ y (2)) (+ z (2))) (| (+ y (2)) (+ x (2)))))) (E. x (A. y (-> (<= (+ y (2)) (+ A (2))) (| (+ y (2)) (+ x (2))))))))
EqReplaceImp1Eq1 # <title> Substitution </title> # <table> # (-> ph (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-> ph (= A [ [ [ C ] )) # </table>
(-> ph (= A B)) , (= B C)(-> ph (= A C))
EqReplaceImp1Eq0 # <title> Substitution </title> # <table> # (-> ph (= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (-> ph (= [ [ [ B ] C)) # </table>
(-> ph (= A C)) , (= A B)(-> ph (= B C))
exfactorial.2 number 52.0 Base case for induction in exfactorial
(E. x (A. y (-> (<= (+ y (1)) (1)) (| (+ y (1)) (+ x (2))))))
exfactoriallem2 number 52.0 Base case for induction in exfactorial
(E. x (A. y (-> (<= (+ y (2)) (2)) (| (+ y (2)) (+ x (2))))))
exfactoriallem4 number 53.0 # <summary> Utility to avoid excessive mandhyp baggage in exfactoriallem3 </summary>
(-> ph (\/ ps ch)) , (-> th ps)(-> (-> ch th) (-> ph ps))
BiReplaceImp0Or1 # <title> Substitution </title> # <table> # (-> (\/ ph [ ps ] ] ] ) th) # (<-> [ ps ] [ ch ] ) # (-> (\/ ph [ [ [ ch ] ) th) # </table>
(-> (\/ ph ps) th) , (<-> ps ch)(-> (\/ ph ch) th)
EqReplaceImp0Or1Le1 # <title> Substitution </title> # <table> # (-> (\/ ph (<= A [ B ] ] ] )) ps) # (= [ B ] [ C ] ) # (-> (\/ ph (<= A [ [ [ C ] )) ps) # </table>
(-> (\/ ph (<= A B)) ps) , (= B C)(-> (\/ ph (<= A C)) ps)
EqReplaceImp0Or1Le1Add1 # <title> Substitution </title> # <table> # (-> (\/ ph (<= A (+ B [ C ] ] ] ))) ps) # (= [ C ] [ D ] ) # (-> (\/ ph (<= A (+ B [ [ [ D ] ))) ps) # </table>
(-> (\/ ph (<= A (+ B C))) ps) , (= C D)(-> (\/ ph (<= A (+ B D))) ps)
EqReplaceEq1Mul1 # <title> Substitution </title> # <table> # (= A (* B [ C ] ] ] )) # (= [ C ] [ D ] ) # (= A (* B [ [ [ D ] )) # </table>
(= A (* B C)) , (= C D)(= A (* B D))
EqReplaceEq1Add1 # <title> Substitution </title> # <table> # (= A (+ B [ C ] ] ] )) # (= [ C ] [ D ] ) # (= A (+ B [ [ [ D ] )) # </table>
(= A (+ B C)) , (= C D)(= A (+ B D))
BiReplaceImp1Imp1 # <title> Substitution </title> # <table> # (-> ph (-> ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (-> ph (-> ps [ [ [ th ] )) # </table>
(-> ph (-> ps ch)) , (<-> ch th)(-> ph (-> ps th))
EqReplaceImp1Imp1Divs1 # <title> Substitution </title> # <table> # (-> ph (-> ps (| A [ B ] ] ] ))) # (= [ B ] [ C ] ) # (-> ph (-> ps (| A [ [ [ C ] ))) # </table>
(-> ph (-> ps (| A B))) , (= B C)(-> ph (-> ps (| A C)))
exfactorial.3 number 54.0 Inductive step for exfactorial
(-> (E. x (A. y (-> (<= (+ y (1)) (+ z (1))) (| (+ y (1)) (+ x (2)))))) (E. x (A. y (-> (<= (+ y (1)) (+ z (2))) (| (+ y (1)) (+ x (2)))))))
EqReplaceBi1Le1 # <title> Substitution </title> # <table> # (<-> ph (<= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (<-> ph (<= A [ [ [ C ] )) # </table>
(<-> ph (<= A B)) , (= B C)(<-> ph (<= A C))
2plus1 # <title> One-digit Addition </title>
(= (+ (2) (1)) (3))
EqReplaceBi1Le1Add1 # <title> Substitution </title> # <table> # (<-> ph (<= A (+ B [ C ] ] ] ))) # (= [ C ] [ D ] ) # (<-> ph (<= A (+ B [ [ [ D ] ))) # </table>
(<-> ph (<= A (+ B C))) , (= C D)(<-> ph (<= A (+ B D)))
1plus2 # <title> One-digit Addition </title>
(= (+ (1) (2)) (3))
exfactoriallem3 number 54.0 Inductive step for exfactorial
(-> (E. x (A. y (-> (<= (+ y (2)) (+ z (2))) (| (+ y (2)) (+ x (2)))))) (E. x (A. y (-> (<= (+ y (2)) (+ z (3))) (| (+ y (2)) (+ x (2)))))))
BiReplaceImp1Bi1 # <title> Substitution </title> # <table> # (-> ph (<-> ps [ ch ] ] ] )) # (<-> [ ch ] [ th ] ) # (-> ph (<-> ps [ [ [ th ] )) # </table>
(-> ph (<-> ps ch)) , (<-> ch th)(-> ph (<-> ps th))
BiReplaceImp1Bi1Ex1 # <title> Substitution </title> # <table> # (-> ph (<-> ps (E. x [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (-> ph (<-> ps (E. x [ [ [ th ] ))) # </table>
(-> ph (<-> ps (E. x ch))) , (<-> ch th)(-> ph (<-> ps (E. x th)))
BiReplaceImp1Bi1Ex1Al1 # <title> Substitution </title> # <table> # (-> ph (<-> ps (E. x (A. y [ ch ] ] ] )))) # (<-> [ ch ] [ th ] ) # (-> ph (<-> ps (E. x (A. y [ [ [ th ] )))) # </table>
(-> ph (<-> ps (E. x (A. y ch)))) , (<-> ch th)(-> ph (<-> ps (E. x (A. y th))))
BiReplaceImp1Bi1Ex1Al1Imp0 # <title> Substitution </title> # <table> # (-> ph (<-> ps (E. x (A. y (-> [ ch ] ] ] ta))))) # (<-> [ ch ] [ th ] ) # (-> ph (<-> ps (E. x (A. y (-> [ [ [ th ] ta))))) # </table>
(-> ph (<-> ps (E. x (A. y (-> ch ta))))) , (<-> ch th)(-> ph (<-> ps (E. x (A. y (-> th ta)))))
EqReplaceImp1Bi1Ex1Al1Imp0Le1 # <title> Substitution </title> # <table> # (-> ph (<-> ps (E. x (A. y (-> (<= A [ B ] ] ] ) ch))))) # (= [ B ] [ C ] ) # (-> ph (<-> ps (E. x (A. y (-> (<= A [ [ [ C ] ) ch))))) # </table>
(-> ph (<-> ps (E. x (A. y (-> (<= A B) ch))))) , (= B C)(-> ph (<-> ps (E. x (A. y (-> (<= A C) ch)))))
EqReplaceImp1Bi1Ex1Al1Imp0Le1Add1 # <title> Substitution </title> # <table> # (-> ph (<-> ps (E. x (A. y (-> (<= A (+ B [ C ] ] ] )) ch))))) # (= [ C ] [ D ] ) # (-> ph (<-> ps (E. x (A. y (-> (<= A (+ B [ [ [ D ] )) ch))))) # </table>
(-> ph (<-> ps (E. x (A. y (-> (<= A (+ B C)) ch))))) , (= C D)(-> ph (<-> ps (E. x (A. y (-> (<= A (+ B D)) ch)))))
exfactorial # <summary> # There exists a number that is divided all numbers up to #(+ A (1))#. While factorial is # certainly one such, it's not the only, so perhaps this is not an ideal name. # </summary>
(E. x (A. y (-> (<= (+ y (1)) (+ A (1))) (| (+ y (1)) (+ x (2))))))
BiReplaceImp1Imp1Ex1 # <title> Substitution </title> # <table> # (-> ph (-> ps (E. x [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (-> ph (-> ps (E. x [ [ [ th ] ))) # </table>
(-> ph (-> ps (E. x ch))) , (<-> ch th)(-> ph (-> ps (E. x th)))
EqReplaceImp1Imp1Ex1Eq0 # <title> Substitution </title> # <table> # (-> ph (-> ps (E. x (= [ A ] ] ] C)))) # (= [ A ] [ B ] ) # (-> ph (-> ps (E. x (= [ [ [ B ] C)))) # </table>
(-> ph (-> ps (E. x (= A C)))) , (= A B)(-> ph (-> ps (E. x (= B C))))
EqReplaceEq0 # <title> Substitution </title> # <table> # (= [ A ] ] ] C) # (= [ A ] [ B ] ) # (= [ [ [ B ] C) # </table>
(= A C) , (= A B)(= B C)
EqReplaceImp0Divs1 # <title> Substitution </title> # <table> # (-> (| A [ B ] ] ] ) ph) # (= [ B ] [ C ] ) # (-> (| A [ [ [ C ] ) ph) # </table>
(-> (| A B) ph) , (= B C)(-> (| A C) ph)
EqReplaceImp1Relprim0 # <title> Substitution </title> # <table> # (-> ph (relprim [ A ] ] ] C)) # (= [ A ] [ B ] ) # (-> ph (relprim [ [ [ B ] C)) # </table>
(-> ph (relprim A C)) , (= A B)(-> ph (relprim B C))
EqReplaceImp1Relprim0Add0 # <title> Substitution </title> # <table> # (-> ph (relprim (+ [ A ] ] ] C) D)) # (= [ A ] [ B ] ) # (-> ph (relprim (+ [ [ [ B ] C) D)) # </table>
(-> ph (relprim (+ A C) D)) , (= A B)(-> ph (relprim (+ B C) D))
EqReplaceImp1Relprim0Add0Mul1 # <title> Substitution </title> # <table> # (-> ph (relprim (+ (* A [ B ] ] ] ) D) A')) # (= [ B ] [ C ] ) # (-> ph (relprim (+ (* A [ [ [ C ] ) D) A')) # </table>
(-> ph (relprim (+ (* A B) D) A')) , (= B C)(-> ph (relprim (+ (* A C) D) A'))
EqReplaceImp1Relprim1 # <title> Substitution </title> # <table> # (-> ph (relprim A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-> ph (relprim A [ [ [ C ] )) # </table>
(-> ph (relprim A B)) , (= B C)(-> ph (relprim A C))
EqReplaceImp1Relprim1Add0 # <title> Substitution </title> # <table> # (-> ph (relprim A (+ [ B ] ] ] D))) # (= [ B ] [ C ] ) # (-> ph (relprim A (+ [ [ [ C ] D))) # </table>
(-> ph (relprim A (+ B D))) , (= B C)(-> ph (relprim A (+ C D)))
EqReplaceImp1Relprim1Add0Mul1 # <title> Substitution </title> # <table> # (-> ph (relprim A (+ (* B [ C ] ] ] ) A'))) # (= [ C ] [ D ] ) # (-> ph (relprim A (+ (* B [ [ [ D ] ) A'))) # </table>
(-> ph (relprim A (+ (* B C) A'))) , (= C D)(-> ph (relprim A (+ (* B D) A')))
beta.2.1 number 134.5
(E. w (A. x (A. y (-> (/\ (<= y x) (/\ (-. (= x y)) (/\ (< x A) (< y A)))) (relprim (+ (* x (+ w (2))) (1)) (+ (* y (+ w (2))) (1)))))))
beta.2 number 135.0
(E. w (A. x (A. y (-> (/\ (-. (= x y)) (/\ (< x A) (< y A))) (relprim (+ (* x (+ w (2))) (1)) (+ (* y (+ w (2))) (1)))))))
beta.2s number 135.1
(E. w (A. x (A. y (-> (/\ (-. (= x y)) (/\ (< x A) (< y A))) (relprim (+ (* (+ x (1)) (+ w (2))) (1)) (+ (* (+ y (1)) (+ w (2))) (1)))))))
beta.3.1 number 137.5
(<-> ph (E. x' (/\ ps (= x (+ (* (+ x' (1)) (+ A (1))) (1))))))(-> ph (< (1) x))
BiReplaceBi1Ex1 # <title> Substitution </title> # <table> # (<-> ph (E. x [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (<-> ph (E. x [ [ [ ch ] )) # </table>
(<-> ph (E. x ps)) , (<-> ps ch)(<-> ph (E. x ch))
BiReplaceBi1Ex1An1 # <title> Substitution </title> # <table> # (<-> ph (E. x (/\ ps [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (<-> ph (E. x (/\ ps [ [ [ th ] ))) # </table>
(<-> ph (E. x (/\ ps ch))) , (<-> ch th)(<-> ph (E. x (/\ ps th)))
EqReplaceBi1Ex1An1Eq1 # <title> Substitution </title> # <table> # (<-> ph (E. x (/\ ps (= A [ B ] ] ] )))) # (= [ B ] [ C ] ) # (<-> ph (E. x (/\ ps (= A [ [ [ C ] )))) # </table>
(<-> ph (E. x (/\ ps (= A B)))) , (= B C)(<-> ph (E. x (/\ ps (= A C))))
EqReplaceBi1Ex1An1Eq1Add0 # <title> Substitution </title> # <table> # (<-> ph (E. x (/\ ps (= A (+ [ B ] ] ] D))))) # (= [ B ] [ C ] ) # (<-> ph (E. x (/\ ps (= A (+ [ [ [ C ] D))))) # </table>
(<-> ph (E. x (/\ ps (= A (+ B D))))) , (= B C)(<-> ph (E. x (/\ ps (= A (+ C D)))))
EqReplaceBi1Ex1An1Eq1Add0Mul1 # <title> Substitution </title> # <table> # (<-> ph (E. x (/\ ps (= A (+ (* B [ C ] ] ] ) A'))))) # (= [ C ] [ D ] ) # (<-> ph (E. x (/\ ps (= A (+ (* B [ [ [ D ] ) A'))))) # </table>
(<-> ph (E. x (/\ ps (= A (+ (* B C) A'))))) , (= C D)(<-> ph (E. x (/\ ps (= A (+ (* B D) A')))))
EqReplaceBi1Ex1An1Eq1Add0Mul1Add1 # <title> Substitution </title> # <table> # (<-> ph (E. x (/\ ps (= A (+ (* B (+ C [ D ] ] ] )) B'))))) # (= [ D ] [ A' ] ) # (<-> ph (E. x (/\ ps (= A (+ (* B (+ C [ [ [ A' ] )) B'))))) # </table>
(<-> ph (E. x (/\ ps (= A (+ (* B (+ C D)) B'))))) , (= D A')(<-> ph (E. x (/\ ps (= A (+ (* B (+ C A')) B')))))
BiReplaceImp0Ex1 # <title> Substitution </title> # <table> # (-> (E. x [ ph ] ] ] ) ch) # (<-> [ ph ] [ ps ] ) # (-> (E. x [ [ [ ps ] ) ch) # </table>
(-> (E. x ph) ch) , (<-> ph ps)(-> (E. x ps) ch)
BiReplaceImp0Ex1Ex1 # <title> Substitution </title> # <table> # (-> (E. x (E. y [ ph ] ] ] )) ch) # (<-> [ ph ] [ ps ] ) # (-> (E. x (E. y [ [ [ ps ] )) ch) # </table>
(-> (E. x (E. y ph)) ch) , (<-> ph ps)(-> (E. x (E. y ps)) ch)
BiReplaceImp0Ex1Ex1An0 # <title> Substitution </title> # <table> # (-> (E. x (E. y (/\ [ ph ] ] ] ch))) th) # (<-> [ ph ] [ ps ] ) # (-> (E. x (E. y (/\ [ [ [ ps ] ch))) th) # </table>
(-> (E. x (E. y (/\ ph ch))) th) , (<-> ph ps)(-> (E. x (E. y (/\ ps ch))) th)
BiReplaceImp0Ex1Ex1An0Al1 # <title> Substitution </title> # <table> # (-> (E. x (E. y (/\ (A. z [ ph ] ] ] ) ch))) th) # (<-> [ ph ] [ ps ] ) # (-> (E. x (E. y (/\ (A. z [ [ [ ps ] ) ch))) th) # </table>
(-> (E. x (E. y (/\ (A. z ph) ch))) th) , (<-> ph ps)(-> (E. x (E. y (/\ (A. z ps) ch))) th)
BiReplaceImp0Ex1Ex1An0Al1Imp0 # <title> Substitution </title> # <table> # (-> (E. x (E. y (/\ (A. z (-> [ ph ] ] ] ch)) th))) ta) # (<-> [ ph ] [ ps ] ) # (-> (E. x (E. y (/\ (A. z (-> [ [ [ ps ] ch)) th))) ta) # </table>
(-> (E. x (E. y (/\ (A. z (-> ph ch)) th))) ta) , (<-> ph ps)(-> (E. x (E. y (/\ (A. z (-> ps ch)) th))) ta)
BiReplaceImp0Ex1Ex1An0Al1Imp0An0 # <title> Substitution </title> # <table> # (-> (E. x (E. y (/\ (A. z (-> (/\ [ ph ] ] ] ch) th)) ta))) et) # (<-> [ ph ] [ ps ] ) # (-> (E. x (E. y (/\ (A. z (-> (/\ [ [ [ ps ] ch) th)) ta))) et) # </table>
(-> (E. x (E. y (/\ (A. z (-> (/\ ph ch) th)) ta))) et) , (<-> ph ps)(-> (E. x (E. y (/\ (A. z (-> (/\ ps ch) th)) ta))) et)
EqReplaceImp0Ex1Ex1An0Al1Imp0An0Lt1 # <title> Substitution </title> # <table> # (-> (E. x (E. y (/\ (A. z (-> (/\ (< A [ B ] ] ] ) ph) ps)) ch))) th) # (= [ B ] [ C ] ) # (-> (E. x (E. y (/\ (A. z (-> (/\ (< A [ [ [ C ] ) ph) ps)) ch))) th) # </table>
(-> (E. x (E. y (/\ (A. z (-> (/\ (< A B) ph) ps)) ch))) th) , (= B C)(-> (E. x (E. y (/\ (A. z (-> (/\ (< A C) ph) ps)) ch))) th)
EqReplaceImp0Ex1Ex1An0Al1Imp0An0Lt1Add1 # <title> Substitution </title> # <table> # (-> (E. x (E. y (/\ (A. z (-> (/\ (< A (+ B [ C ] ] ] )) ph) ps)) ch))) th) # (= [ C ] [ D ] ) # (-> (E. x (E. y (/\ (A. z (-> (/\ (< A (+ B [ [ [ D ] )) ph) ps)) ch))) th) # </table>
(-> (E. x (E. y (/\ (A. z (-> (/\ (< A (+ B C)) ph) ps)) ch))) th) , (= C D)(-> (E. x (E. y (/\ (A. z (-> (/\ (< A (+ B D)) ph) ps)) ch))) th)
beta.3 number 138.0 # <summary> A development of Godel's Beta Function, following Shoenfield(1967). </summary>
(<-> ph (E. x' (/\ (/\ (<= x' A) (e. x' S)) (= x (+ (* (+ x' (1)) (+ w (2))) (1)))))) , (<-> ps (E. y' (/\ (/\ (<= y' B) (-. (e. y' S))) (= y (+ (* (+ y' (1)) (+ w (2))) (1))))))(E. w (E. z' (/\ (A. x (-> ph (| x z'))) (A. y (-> ps (-. (| y z')))))))
beta.4.1 number 139.5
(-> (A. x (-> (E. x' (/\ ph (= x B))) (| x A))) (A. x' (-> ph (| B A))))
beta.4.2 number 139.6
(-> (A. x (-> (E. x' (/\ ph (= x B))) (-. (| x A)))) (A. x' (-> ph (-. (| B A)))))
beta.4 number 140.0
(E. z (A. x' (-> (<= x' A) (<-> (e. x' S) (| (+ (* (+ x' (1)) (tail z)) (1)) (head z))))))
maxex2 number 143.0
(-> (fun S) (E. v (A. w (-> (/\ (< (head w) A) (e. w S)) (<= w (<,> A v))))))
beta number 146.0 # <summary> # A development of Godel's Beta Function, following Shoenfield(1967). # If S is a functional set defining a sequence {S(0), S(1), ..., S(A), ...}: # Then there exists a z such that for all x in [0,A], we have: # beta(z, x) = S(x). # This allows us to encode finite sequences in a quantifiable way, # which is necessary to deal with recursive functions. # </summary>
(-> (fun S) (E. z (A. x (-> (< x A) (e. (<,> x (beta z x)) S)))))

## Recursive functions

df-recursep-just Definition of recursion, using a predicate. (recursep S A B C) will mean that S^A(B) = C
(<-> (E. z (/\ (= (beta z (0)) B) (/\ (= (beta z A) C) (A. y (-> (< y A) (e. (<,> (beta z y) (beta z (+ y (1)))) S)))))) (E. w (/\ (= (beta w (0)) B) (/\ (= (beta w A) C) (A. x (-> (< x A) (e. (<,> (beta w x) (beta w (+ x (1)))) S)))))))
df-recursep # <title> Definition of Recursive Predicate </title> # <suggest> right('Define', 'rec') left('Simplify', 'rec') </suggest>
(<-> (recursep S A B C) (E. z (/\ (= (beta z (0)) B) (/\ (= (beta z A) C) (A. y (-> (< y A) (e. (<,> (beta z y) (beta z (+ y (1)))) S)))))))
recursepeq4 # <title> Fourth equality identity for recursep </title>
(-> (= A B) (<-> (recursep S C D A) (recursep S C D B)))
recursive.3.1 number 160.0
(<-> ph (/\ (A. y (-> (<= y (+ A (1))) (\/ (/\ (<= y A) (= (beta z y) (beta v y))) (/\ (= y (+ A (1))) (= (beta z y) (apply S C)))))) (/\ (= (beta v (0)) B) (/\ (= (beta v A) C) (A. y (-> (< y A) (e. (<,> (beta v y) (beta v (+ y (1)))) S)))))))(-> (fun S) (-> (recursep S A B C) (recursep S (+ A (1)) B (apply S C))))
recursive.3 number 161.0
(-> (-> (fun S) (E. x (recursep S w A x))) (-> (fun S) (E. x (recursep S (+ w (1)) A x))))
(-> (= w B) (<-> (-> (fun S) (E. x (recursep S w A x))) (-> (fun S) (E. x (recursep S B A x)))))
recursive.2.1 number 152.0
(E. x (= (beta x (0)) A))
recursive.2 Base case
(-> (fun S) (E! x (E. z (/\ (= (beta z (0)) A) (/\ (= (beta z (0)) x) (A. y (-> (< y (0)) (e. (<,> (beta x y) (beta x (+ y (1)))) S))))))))
recursive.2a Base case
(-> (fun S) (E. x (recursep S (0) A x)))
recursive # <summary> Existence of the result of a recursion operation. </summary>
(-> (fun S) (E. w (recursep S A B w)))
recursep-uniq.1 number 166.0
(-> (fun S) (<-> (recursep S (0) A B) (= A B)))
recursepsuc # <summary> Recursing "one more time" works as expected. </summary>
(-> (recursep S (+ A (1)) B C) (E. x (/\ (recursep S A B x) (e. (<,> x C) S))))
(-> (fun S) (-> (A. z (A. z' (-> (/\ (recursep S y A z) (recursep S y A z')) (= z z')))) (A. z (A. z' (-> (/\ (recursep S (+ y (1)) A z) (recursep S (+ y (1)) A z')) (= z z'))))))
recursepeq2 Second equality identitiy for recursep.
(-> (= A B) (<-> (recursep S A C D) (recursep S B C D)))
recursep-uniq.3 number 170.0
(-> (= x B) (<-> (-> (fun S) (A. z (A. z' (-> (/\ (recursep S x A z) (recursep S x A z')) (= z z'))))) (-> (fun S) (A. z (A. z' (-> (/\ (recursep S B A z) (recursep S B A z')) (= z z')))))))
recursep-uniq # <summary> Uniqueness of the result of a recursion operation. </summary>
(-> (fun S) (-> (/\ (recursep S A B C) (recursep S A B D)) (= C D)))
recursepeq1 First equality identity of recursep.
(-> (=_ S T) (<-> (recursep S A B C) (recursep T A B C)))
recursep0 # <title> Recursing zero times does nothing </title> # <suggest> full('Simplify', 'T') </suggest>
(recursep S (0) A A)
eurecursep number 174.0 # <summary> # There exists a unique answer to recursing the function S exactly B times # starting at A. # </summary>
(-> (fun S) (E! x (recursep S A B x)))
(= (iota ({|} x (recursep S A B x))) (iota ({|} z (recursep S A B z))))
df-recurse # <title> Definition of Recursive Function </title> # <suggest> right('Define', 're') left('Simplify', 're') </suggest>
(= (recurse S A B) (iota ({|} x (recursep S A B x))))
recurseseq1 First equality identity for recurse
(-> (=_ S T) (= (recurse S A B) (recurse T A B)))
recurseeq2 Second equality identity for recurse
(-> (= A B) (= (recurse S A C) (recurse S B C)))
BiReplaceImp1Bi0 # <title> Substitution </title> # <table> # (-> ph (<-> [ ps ] ] ] th)) # (<-> [ ps ] [ ch ] ) # (-> ph (<-> [ [ [ ch ] th)) # </table>
(-> ph (<-> ps th)) , (<-> ps ch)(-> ph (<-> ch th))
recursepseq1 # <title> Equivalence for recursep </title> ##
(-> (=_ S T) (<-> (recursep S A B C) (recursep T A B C)))
(=_ S T)(<-> (recursep S A B C) (recursep T A B C))
(-> ph (=_ S T))(-> ph (<-> (recursep S A B C) (recursep T A B C)))
(= A B)(<-> (recursep S A C D) (recursep S B C D))
(-> ph (= A B))(-> ph (<-> (recursep S A C D) (recursep S B C D)))
recursepeq3 # <title> Equivalence for recursep </title> ##
(-> (= B D) (<-> (recursep S A B C) (recursep S A D C)))
(= B D)(<-> (recursep S A B C) (recursep S A D C))
(-> ph (= B D))(-> ph (<-> (recursep S A B C) (recursep S A D C)))
(= A B)(<-> (recursep S C D A) (recursep S C D B))
(-> ph (= A B))(-> ph (<-> (recursep S C D A) (recursep S C D B)))
(=_ S T)(= (recurse S A B) (recurse T A B))
(-> ph (=_ S T))(-> ph (= (recurse S A B) (recurse T A B)))
(= A B)(= (recurse S A C) (recurse S B C))
(-> ph (= A B))(-> ph (= (recurse S A C) (recurse S B C)))
recurseeq3 # <title> Equivalence for recurse </title> ##
(-> (= B C) (= (recurse S A B) (recurse S A C)))
(= B C)(= (recurse S A B) (recurse S A C))
(-> ph (= B C))(-> ph (= (recurse S A B) (recurse S A C)))
(-> (/\ (= A B) (= C D)) (= (recurse S A C) (recurse S B D)))
SeqReplaceImp1Eq1Iota0 # <title> Substitution </title> # <table> # (-> ph (= A (iota [ S ] ] ] ))) # (=_ [ S ] [ T ] ) # (-> ph (= A (iota [ [ [ T ] ))) # </table>
(-> ph (= A (iota S))) , (=_ S T)(-> ph (= A (iota T)))
recurseNoPred # <title> Convert a recurse predicate to recurse </title>
(-> (/\ (fun S) (recursep S A B C)) (= (recurse S A B) C))
recurseNoPredi # <title> Convert a recurse predicate to recurse </title>
(fun S)(-> (recursep S A B C) (= (recurse S A B) C))
EqReplaceImp0Recursep1 # <title> Substitution </title> # <table> # (-> (recursep S [ A ] ] ] C D) ph) # (= [ A ] [ B ] ) # (-> (recursep S [ [ [ B ] C D) ph) # </table>
(-> (recursep S A C D) ph) , (= A B)(-> (recursep S B C D) ph)
ImpReplaceImp1Ex1 # <title> Substitution </title> # <table> # (-> ph (E. x [ ps ] ] ] )) # (-> [ ps ] [ ch ] ) # (-> ph (E. x [ [ [ ch ] )) # </table>
(-> ph (E. x ps)) , (-> ps ch)(-> ph (E. x ch))
ImpReplaceImp1Ex1An0 # <title> Substitution </title> # <table> # (-> ph (E. x (/\ [ ps ] ] ] th))) # (-> [ ps ] [ ch ] ) # (-> ph (E. x (/\ [ [ [ ch ] th))) # </table>
(-> ph (E. x (/\ ps th))) , (-> ps ch)(-> ph (E. x (/\ ch th)))
recurse0 # <title> Applying a Function 0 Times </title>
(-> (fun S) (= (recurse S (0) A) A))
recurse0i # <title> Applying a Function 0 Times </title>
(fun S)(= (recurse S (0) A) A)
BiReplaceBi0An0 # <title> Substitution </title> # <table> # (<-> (/\ [ ph ] ] ] ch) th) # (<-> [ ph ] [ ps ] ) # (<-> (/\ [ [ [ ps ] ch) th) # </table>
(<-> (/\ ph ch) th) , (<-> ph ps)(<-> (/\ ps ch) th)
BiReplaceImp1Ex1 # <title> Substitution </title> # <table> # (-> ph (E. x [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-> ph (E. x [ [ [ ch ] )) # </table>
(-> ph (E. x ps)) , (<-> ps ch)(-> ph (E. x ch))
recursesuc # <title> Recursion Applies a Function Multiple Times </title>
(fun S)(= (recurse S (+ A (1)) B) (apply S (recurse S A B)))
emptyThm # <summary> This is used just for convenience to get an empty theorem. </summary>
(T)