param (PROP prop.ghi () "") param (PREDICATE ../predicate/predicate_equals.ghi (PROP) "") tvar (wff ph ps ch th ta) tvar (nat A B C D A' B') term (nat (head A)) term (nat (tail A)) term (nat (<,> A B)) ## Apply Head Operator ## right('Simplify', 'Hd') stmt (headop () () (= (head (<,> A B)) A)) ## Apply Tail Operator ## right('Simplify', 'Tl') stmt (tailop () () (= (tail (<,> A B)) B)) ## Equality theorem for head stmt (headeq () () (-> (= A B) (= (head A) (head B)))) ## Equality theorem for tail stmt (taileq () () (-> (= A B) (= (tail A) (tail B)))) ## Equality theorem for head stmt (headeqi () ((= A B)) (= (head A) (head B))) ## Equality theorem for tail stmt (taileqi () ((= A B)) (= (tail A) (tail B))) stmt (headeqd () ((-> ph (= A B))) (-> ph (= (head A) (head B)))) stmt (taileqd () ((-> ph (= A B))) (-> ph (= (tail A) (tail B)))) ## Ordered Pair Equality stmt (opeq1 () () (-> (= A B) (= (<,> A C) (<,> B C)))) ## Ordered Pair Equality stmt (opeq2 () () (-> (= A B) (= (<,> C A) (<,> C B)))) stmt (opeq1i () ((= A B)) (= (<,> A C) (<,> B C))) stmt (opeq1d () ((-> ph (= A B))) (-> ph (= (<,> A C) (<,> B C)))) stmt (opeq2i () ((= A B)) (= (<,> C A) (<,> C B))) stmt (opeq2d () ((-> ph (= A B))) (-> ph (= (<,> C A) (<,> C B)))) ## Ordered Pair Equality stmt (opeq12 () () (-> (/\ (= A B) (= C D)) (= (<,> A C) (<,> B D)))) ## Ordered Pair Equality stmt (opeq12d () ((-> ph (= A B)) (-> ph (= C D))) (-> ph (= (<,> A C) (<,> B D)))) ## Expand Ordered Pair stmt (opexpand () () (= A (<,> (head A) (tail A)))) ## Ordered Pair Theorem ## ## Two ordered pairs are equal if and only if the first and the ## second numbers of the pair are equal. ## stmt (opth () () (<-> (= (<,> A B) (<,> A' B')) (/\ (= A A') (= B B'))))