# List of theorems

List of theorems in peano_new/function.gh:

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))
df-apply-just number 157.5 # <summary> # Definition of "apply" to apply a function (reperesented by a set S) to an # input. # </summary>
(= (iota ({|} z (e. (<,> A z) S))) (iota ({|} y (e. (<,> A y) S))))
df-apply Definition of function application
(= (apply S A) (iota ({|} z (e. (<,> A z) S))))
applyseq1 # <title> Equivalence for apply </title> ##
(-> (=_ S T) (= (apply S A) (apply T A)))
(=_ S T)(= (apply S A) (apply T A))
(-> ph (=_ S T))(-> ph (= (apply S A) (apply T A)))
applyeq2 # <title> Equivalence for apply </title> ##
(-> (= A B) (= (apply S A) (apply S B)))
(= A B)(= (apply S A) (apply S B))
(-> ph (= A B))(-> ph (= (apply S A) (apply S B)))
df-fun-just number 86.0
(<-> (/\ (A. x (E! y (e. (<,> x y) S))) (A. x (-> (e. x S) (E. y (E. z (= x (<,> y z))))))) (/\ (A. x' (E! y' (e. (<,> x' y') S))) (A. x' (-> (e. x' S) (E. y' (E. z' (= x' (<,> y' z'))))))))
df-fun # <title> Function Definition </title> # <summary> # Functions are represented by sets of ordered pairs, but not every set is a valid function. # fun S is true when the set S is a valid function and false otherwise. # </summary>
(<-> (fun S) (/\ (A. x (E! y (e. (<,> x y) S))) (A. x (-> (e. x S) (E. y (E. z (= x (<,> y z))))))))
funseq Equality identity for fun
(-> (=_ S T) (<-> (fun S) (fun T)))
(=_ S T)(<-> (fun S) (fun T))
(-> ph (=_ S T))(-> ph (<-> (fun S) (fun T)))

## Lambda and function application

df-lambda-just # <summary> # Definition of the lambda operator, which creates a functional set from an # expression in one variable. # </summary>
(=_ ({|} x (E. y (= x (<,> y A)))) ({|} x' (E. y (= x' (<,> y A)))))
(=_ (lambda y A) ({|} x (E. y (= x (<,> y A)))))
ellambda # <summary> Asserts that membership in functional set of a lambda works the way you'd expect. </summary>
(-> (= x y) (= B C))(<-> (e. (<,> x A) (lambda x B)) (= A B))
funlambda # <title> Lambda constructs are functions </title>
(-> (= x y) (= A B))(fun (lambda x A))
piecewisefun.1 number 156.5
(<-> (e. A ({|} x (\/ (/\ ([/] (head x) x ph) (e. x S)) (/\ (-. ([/] (head x) x ph)) (e. x T))))) (\/ (/\ ([/] (head A) x ph) (e. A S)) (/\ (-. ([/] (head A) x ph)) (e. A T))))
piecewisefun number 157.0 # <summary> # Given two functions S, T and a discriminator ph, we can assemble a piecewise # function which mimics S when ph is true and T otherwise. # </summary>
(-> (/\ (fun S) (fun T)) (fun ({|} x' (\/ (/\ ([/] (head x') x' ph) (e. x' S)) (/\ (-. ([/] (head x') x' ph)) (e. x' T))))))
funapply number 159.5 # <summary> apply actually works (assuming S is a function). </summary>
(-> (fun S) (e. (<,> A (apply S A)) S))
(-> (= x y) (= A B))(= (apply (lambda x A) x) A)
(-> (= x y) (= A B))(-> (= x C) (= (apply (lambda x A) C) A))
applylambda # <title> Apply the function </title>
(-> (= x y) (= B D)) , (-> (= x A) (= B C))(= (apply (lambda x B) A) C)
applylambdaconst # <title> Apply a constant function </title>
(= (apply (lambda x A) B) A)
applyfunid # <title> Apply the identity function </title>
(= (apply (lambda x x) A) A)
(-> ph (=_ S T)) , (=_ U T)(-> ph (=_ S U))
lambdaeq1 First equality identity for lambda.
(-> (= x y) (= A B))(=_ (lambda x A) (lambda y B))
lambdaeq2 Second equality identity for lambda
(-> (A. x (= A B)) (=_ (lambda x A) (lambda x B)))
(A. x (= B C))(=_ (lambda x B) (lambda x C))
(-> ph (A. x (= B C)))(-> ph (=_ (lambda x B) (lambda x C)))
emptyThm # <summary> This is used just for convenience to get an empty theorem. </summary>
(T)