# List of theorems

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

(=_ 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)))
(= 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)))
EqReplaceEq0 # <title> Substitution </title> # <table> # (= [ A ] ] ] C) # (= [ A ] [ B ] ) # (= [ [ [ B ] C) # </table>
(= A C) , (= A B)(= B C)
EqReplaceEq0Recurse1 # <title> Substitution </title> # <table> # (= (recurse S [ A ] ] ] C) D) # (= [ A ] [ B ] ) # (= (recurse S [ [ [ B ] C) D) # </table>
(= (recurse S A C) D) , (= A B)(= (recurse S B C) D)
EqReplaceEq1Apply1 # <title> Substitution </title> # <table> # (= A (apply S [ B ] ] ] )) # (= [ B ] [ C ] ) # (= A (apply S [ [ [ C ] )) # </table>
(= A (apply S B)) , (= B C)(= A (apply S C))
recurse1 # <title> Applying a Function Once </title>
(fun S)(= (recurse S (1) A) (apply S A))
(<-> ([/] A x (= (recurse S x (recurse S B C)) (recurse S (+ x B) C))) (= (recurse S A (recurse S B C)) (recurse S (+ A B) C)))
EqReplaceImp1Eq0 # <title> Substitution </title> # <table> # (-> ph (= [ A ] ] ] C)) # (= [ A ] [ B ] ) # (-> ph (= [ [ [ B ] C)) # </table>
(-> ph (= A C)) , (= A B)(-> ph (= B C))
EqReplaceImp1Eq1 # <title> Substitution </title> # <table> # (-> ph (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-> ph (= A [ [ [ C ] )) # </table>
(-> ph (= A B)) , (= B C)(-> ph (= A C))
EqReplaceImp1Eq1Recurse1 # <title> Substitution </title> # <table> # (-> ph (= A (recurse S [ B ] ] ] D))) # (= [ B ] [ C ] ) # (-> ph (= A (recurse S [ [ [ C ] D))) # </table>
(-> ph (= A (recurse S B D))) , (= B C)(-> ph (= A (recurse S C D)))
EqReplaceImp1Eq1Recurse1Add1 # <title> Substitution </title> # <table> # (-> ph (= A (recurse S (+ B [ C ] ] ] ) A'))) # (= [ C ] [ D ] ) # (-> ph (= A (recurse S (+ B [ [ [ D ] ) A'))) # </table>
(-> ph (= A (recurse S (+ B C) A'))) , (= C D)(-> ph (= A (recurse S (+ B D) A')))
(fun S)(= (recurse S A (recurse S B C)) (recurse S (+ A B) C))
emptyThm # <summary> This is used just for convenience to get an empty theorem. </summary>
(T)