List of theorems

List of theorems in peano_new/arithmetic/integers/mulcan_min.gh:

NeqReplaceBi1Neq0 # <title> Substitution </title> # <table> # (<-> ph (n.= [ A ] ] ] C)) # (n.= [ A ] [ B ] ) # (<-> ph (n.= [ [ [ B ] C)) # </table>
(<-> ph (n.= a c)) , (n.= a b)(<-> ph (n.= b c))
NeqReplaceBi1Neq1 # <title> Substitution </title> # <table> # (<-> ph (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (<-> ph (= A [ [ [ C ] )) # </table>
(<-> ph (n.= a b)) , (n.= b c)(<-> ph (n.= a c))
NeqReplaceBi1Neq0Add0 # <title> Substitution </title> # <table> # (<-> ph (n.= (n.+ [ A ] ] ] C) D)) # (n.= [ A ] [ B ] ) # (<-> ph (n.= (n.+ [ [ [ B ] C) D)) # </table>
(<-> ph (n.= (n.+ a c) d)) , (n.= a b)(<-> ph (n.= (n.+ b c) d))
NeqReplaceBi1Neq0Add1 # <title> Substitution </title> # <table> # (<-> ph (n.= (n.+ a [ B ] ] ] ) D)) # (n.= [ B ] [ C ] ) # (<-> ph (n.= (n.+ a [ [ [ C ] ) D)) # </table>
(<-> ph (n.= (n.+ a b) d)) , (n.= b c)(<-> ph (n.= (n.+ a c) d))
NeqReplaceBi1Neq1Add0 # <title> Substitution </title> # <table> # (<-> ph (n.= a (n.+ [ B ] ] ] D))) # (n.= [ B ] [ C ] ) # (<-> ph (n.= a (n.+ [ [ [ C ] D))) # </table>
(<-> ph (n.= a (n.+ b d))) , (n.= b c)(<-> ph (n.= a (n.+ c d)))
NeqReplaceBi1Neq1Add1 # <title> Substitution </title> # <table> # (<-> ph (n.= a (n.+ b [ C ] ] ] ))) # (n.= [ C ] [ D ] ) # (<-> ph (n.= a (n.+ b [ [ [ D ] ))) # </table>
(<-> ph (n.= a (n.+ b c))) , (n.= c d)(<-> ph (n.= a (n.+ b d)))
(<-> (= (* B A) (* C A)) (n.= (n.+ (n.* (n.+ (head B) (tail C)) (head A)) (n.* (n.+ (head C) (tail B)) (tail A))) (n.+ (n.* (n.+ (head C) (tail B)) (head A)) (n.* (n.+ (head B) (tail C)) (tail A)))))
BiReplaceImp1Nex1 # <title> Substitution </title> # <table> # (-> ph (n.E. x [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-> ph (n.E. x [ [ [ ch ] )) # </table>
(-> ph (n.E. x ps)) , (<-> ps ch)(-> ph (n.E. x ch))
BiReplaceImp1Nex1An1 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ ps [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (-> ph (n.E. x (/\ ps [ [ [ th ] ))) # </table>
(-> ph (n.E. x (/\ ps ch))) , (<-> ch th)(-> ph (n.E. x (/\ ps th)))
ImpReplaceImp1Nex1 # <title> Substitution </title> # <table> # (-> ph (n.E. x [ ps ] ] ] )) # (-> [ ps ] [ ch ] ) # (-> ph (n.E. x [ [ [ ch ] )) # </table>
(-> ph (n.E. x ps)) , (-> ps ch)(-> ph (n.E. x ch))
ImpReplaceImp1Nex1An1 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ ps [ ch ] ] ] ))) # (-> [ ch ] [ th ] ) # (-> ph (n.E. x (/\ ps [ [ [ th ] ))) # </table>
(-> ph (n.E. x (/\ ps ch))) , (-> ch th)(-> ph (n.E. x (/\ ps th)))
ImpReplaceImp1Nex1An1An0 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ ps (/\ [ ch ] ] ] ta)))) # (-> [ ch ] [ th ] ) # (-> ph (n.E. x (/\ ps (/\ [ [ [ th ] ta)))) # </table>
(-> ph (n.E. x (/\ ps (/\ ch ta)))) , (-> ch th)(-> ph (n.E. x (/\ ps (/\ th ta))))
ImpReplaceImp1Nex1An1An1 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ ps (/\ ch [ th ] ] ] )))) # (-> [ th ] [ ta ] ) # (-> ph (n.E. x (/\ ps (/\ ch [ [ [ ta ] )))) # </table>
(-> ph (n.E. x (/\ ps (/\ ch th)))) , (-> th ta)(-> ph (n.E. x (/\ ps (/\ ch ta))))
BiReplaceImp1Nex1An1An1 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ ps (/\ ch [ th ] ] ] )))) # (<-> [ th ] [ ta ] ) # (-> ph (n.E. x (/\ ps (/\ ch [ [ [ ta ] )))) # </table>
(-> ph (n.E. x (/\ ps (/\ ch th)))) , (<-> th ta)(-> ph (n.E. x (/\ ps (/\ ch ta))))
BiReplaceImp1Nex1An1Bi1 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ ps (<-> ch [ th ] ] ] )))) # (<-> [ th ] [ ta ] ) # (-> ph (n.E. x (/\ ps (<-> ch [ [ [ ta ] )))) # </table>
(-> ph (n.E. x (/\ ps (<-> ch th)))) , (<-> th ta)(-> ph (n.E. x (/\ ps (<-> ch ta))))
BiReplaceImp1Nex1An1Bi0 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ ps (<-> [ ch ] ] ] ta)))) # (<-> [ ch ] [ th ] ) # (-> ph (n.E. x (/\ ps (<-> [ [ [ th ] ta)))) # </table>
(-> ph (n.E. x (/\ ps (<-> ch ta)))) , (<-> ch th)(-> ph (n.E. x (/\ ps (<-> th ta))))
NeqReplaceImp1Nex1An1Bi0Neq0 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ ps (<-> (n.= [ A ] ] ] C) ch)))) # (n.= [ A ] [ B ] ) # (-> ph (n.E. x (/\ ps (<-> (n.= [ [ [ B ] C) ch)))) # </table>
(-> ph (n.E. x (/\ ps (<-> (n.= a c) ch)))) , (n.= a b)(-> ph (n.E. x (/\ ps (<-> (n.= b c) ch))))
NeqReplaceImp1Nex1An1Bi0Neq0Nadd1 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ ps (<-> (n.= (n.+ a [ B ] ] ] ) D) ch)))) # (n.= [ B ] [ C ] ) # (-> ph (n.E. x (/\ ps (<-> (n.= (n.+ a [ [ [ C ] ) D) ch)))) # </table>
(-> ph (n.E. x (/\ ps (<-> (n.= (n.+ a b) d) ch)))) , (n.= b c)(-> ph (n.E. x (/\ ps (<-> (n.= (n.+ a c) d) ch))))
NeqReplaceImp1Nex1An1Bi0Neq1 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ ps (<-> (n.= a [ B ] ] ] ) ch)))) # (n.= [ B ] [ C ] ) # (-> ph (n.E. x (/\ ps (<-> (n.= a [ [ [ C ] ) ch)))) # </table>
(-> ph (n.E. x (/\ ps (<-> (n.= a b) ch)))) , (n.= b c)(-> ph (n.E. x (/\ ps (<-> (n.= a c) ch))))
NeqReplaceImp1Nex1An1Bi0Neq1Nadd1 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ ps (<-> (n.= a (n.+ b [ C ] ] ] )) ch)))) # (n.= [ C ] [ D ] ) # (-> ph (n.E. x (/\ ps (<-> (n.= a (n.+ b [ [ [ D ] )) ch)))) # </table>
(-> ph (n.E. x (/\ ps (<-> (n.= a (n.+ b c)) ch)))) , (n.= c d)(-> ph (n.E. x (/\ ps (<-> (n.= a (n.+ b d)) ch))))
NeqReplaceImp1Nex1An1Bi0Neq0Nadd0 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ ps (<-> (n.= (n.+ [ A ] ] ] C) D) ch)))) # (n.= [ A ] [ B ] ) # (-> ph (n.E. x (/\ ps (<-> (n.= (n.+ [ [ [ B ] C) D) ch)))) # </table>
(-> ph (n.E. x (/\ ps (<-> (n.= (n.+ a c) d) ch)))) , (n.= a b)(-> ph (n.E. x (/\ ps (<-> (n.= (n.+ b c) d) ch))))
BiReplaceImp1Not0 # <title> Substitution </title> # <table> # (-> ph (-. [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-> ph (-. [ [ [ ch ] )) # </table>
(-> ph (-. ps)) , (<-> ps ch)(-> ph (-. ch))
ImpReplaceImp1Nex1An0 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ [ ps ] ] ] th))) # (-> [ ps ] [ ch ] ) # (-> ph (n.E. x (/\ [ [ [ ch ] th))) # </table>
(-> ph (n.E. x (/\ ps th))) , (-> ps ch)(-> ph (n.E. x (/\ ch th)))
BiReplaceImp1Nex1An0 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ [ ps ] ] ] th))) # (<-> [ ps ] [ ch ] ) # (-> ph (n.E. x (/\ [ [ [ ch ] th))) # </table>
(-> ph (n.E. x (/\ ps th))) , (<-> ps ch)(-> ph (n.E. x (/\ ch th)))
BiReplaceImp1Nex1An0Bi1 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ (<-> ps [ ch ] ] ] ) ta))) # (<-> [ ch ] [ th ] ) # (-> ph (n.E. x (/\ (<-> ps [ [ [ th ] ) ta))) # </table>
(-> ph (n.E. x (/\ (<-> ps ch) ta))) , (<-> ch th)(-> ph (n.E. x (/\ (<-> ps th) ta)))
BiReplaceImp1Nex1Bi0 # <title> Substitution </title> # <table> # (-> ph (n.E. x (<-> [ ps ] ] ] th))) # (<-> [ ps ] [ ch ] ) # (-> ph (n.E. x (<-> [ [ [ ch ] th))) # </table>
(-> ph (n.E. x (<-> ps th))) , (<-> ps ch)(-> ph (n.E. x (<-> ch th)))
ImpReplaceImp1Ex1 # <title> Substitution </title> # <table> # (-> ph (n.E. x [ ps ] ] ] )) # (-> [ ps ] [ ch ] ) # (-> ph (n.E. x [ [ [ ch ] )) # </table>
(-> ph (n.E. x ps)) , (-> ps ch)(-> ph (n.E. x ch))
ImpReplaceImp1Ex1An0 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ [ ps ] ] ] th))) # (-> [ ps ] [ ch ] ) # (-> ph (n.E. x (/\ [ [ [ ch ] th))) # </table>
(-> ph (n.E. x (/\ ps th))) , (-> ps ch)(-> ph (n.E. x (/\ ch th)))
BiReplaceBi1Ex1 # <title> Substitution </title> # <table> # (<-> ph (n.E. x [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (<-> ph (n.E. x [ [ [ ch ] )) # </table>
(<-> ph (n.E. x ps)) , (<-> ps ch)(<-> ph (n.E. x ch))
BiReplaceImp1Ex1 # <title> Substitution </title> # <table> # (-> ph (n.E. x [ ps ] ] ] )) # (<-> [ ps ] [ ch ] ) # (-> ph (n.E. x [ [ [ ch ] )) # </table>
(-> ph (n.E. x ps)) , (<-> ps ch)(-> ph (n.E. x ch))
BiReplaceImp1Ex1An0 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ [ ps ] ] ] th))) # (<-> [ ps ] [ ch ] ) # (-> ph (n.E. x (/\ [ [ [ ch ] th))) # </table>
(-> ph (n.E. x (/\ ps th))) , (<-> ps ch)(-> ph (n.E. x (/\ ch th)))
ImpReplaceImp1Ex1An0An0 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ (/\ [ ps ] ] ] th) ta))) # (-> [ ps ] [ ch ] ) # (-> ph (n.E. x (/\ (/\ [ [ [ ch ] th) ta))) # </table>
(-> ph (n.E. x (/\ (/\ ps th) ta))) , (-> ps ch)(-> ph (n.E. x (/\ (/\ ch th) ta)))
ImpReplaceImp1Ex1An0An1 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ (/\ ps [ ch ] ] ] ) ta))) # (-> [ ch ] [ th ] ) # (-> ph (n.E. x (/\ (/\ ps [ [ [ th ] ) ta))) # </table>
(-> ph (n.E. x (/\ (/\ ps ch) ta))) , (-> ch th)(-> ph (n.E. x (/\ (/\ ps th) ta)))
BiReplaceImp1Ex1An0An1 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ (/\ ps [ ch ] ] ] ) ta))) # (<-> [ ch ] [ th ] ) # (-> ph (n.E. x (/\ (/\ ps [ [ [ th ] ) ta))) # </table>
(-> ph (n.E. x (/\ (/\ ps ch) ta))) , (<-> ch th)(-> ph (n.E. x (/\ (/\ ps th) ta)))
BiReplaceImp1Ex1An0Bi1 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ (<-> ps [ ch ] ] ] ) ta))) # (<-> [ ch ] [ th ] ) # (-> ph (n.E. x (/\ (<-> ps [ [ [ th ] ) ta))) # </table>
(-> ph (n.E. x (/\ (<-> ps ch) ta))) , (<-> ch th)(-> ph (n.E. x (/\ (<-> ps th) ta)))
BiReplaceImp1Ex1An0Bi0 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ (<-> [ ps ] ] ] th) ta))) # (<-> [ ps ] [ ch ] ) # (-> ph (n.E. x (/\ (<-> [ [ [ ch ] th) ta))) # </table>
(-> ph (n.E. x (/\ (<-> ps th) ta))) , (<-> ps ch)(-> ph (n.E. x (/\ (<-> ch th) ta)))
NeqReplaceImp1Ex1An0Bi0Neq0 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ (<-> (n.= [ A ] ] ] C) ps) ch))) # (n.= [ A ] [ B ] ) # (-> ph (n.E. x (/\ (<-> (n.= [ [ [ B ] C) ps) ch))) # </table>
(-> ph (n.E. x (/\ (<-> (n.= a c) ps) ch))) , (n.= a b)(-> ph (n.E. x (/\ (<-> (n.= b c) ps) ch)))
NeqReplaceImp1Ex1An0Bi0Neq0Add1 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ (<-> (n.= (n.+ a [ B ] ] ] ) D) ps) ch))) # (n.= [ B ] [ C ] ) # (-> ph (n.E. x (/\ (<-> (n.= (n.+ a [ [ [ C ] ) D) ps) ch))) # </table>
(-> ph (n.E. x (/\ (<-> (n.= (n.+ a b) d) ps) ch))) , (n.= b c)(-> ph (n.E. x (/\ (<-> (n.= (n.+ a c) d) ps) ch)))
NeqReplaceImp1Ex1An0Bi0Neq1 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ (<-> (n.= a [ B ] ] ] ) ps) ch))) # (n.= [ B ] [ C ] ) # (-> ph (n.E. x (/\ (<-> (n.= a [ [ [ C ] ) ps) ch))) # </table>
(-> ph (n.E. x (/\ (<-> (n.= a b) ps) ch))) , (n.= b c)(-> ph (n.E. x (/\ (<-> (n.= a c) ps) ch)))
NeqReplaceImp1Ex1An0Bi0Neq1Add1 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ (<-> (n.= a (n.+ b [ C ] ] ] )) ps) ch))) # (n.= [ C ] [ D ] ) # (-> ph (n.E. x (/\ (<-> (n.= a (n.+ b [ [ [ D ] )) ps) ch))) # </table>
(-> ph (n.E. x (/\ (<-> (n.= a (n.+ b c)) ps) ch))) , (n.= c d)(-> ph (n.E. x (/\ (<-> (n.= a (n.+ b d)) ps) ch)))
NeqReplaceImp1Ex1An0Bi0Neq0Add0 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ (<-> (n.= (n.+ [ A ] ] ] C) D) ps) ch))) # (n.= [ A ] [ B ] ) # (-> ph (n.E. x (/\ (<-> (n.= (n.+ [ [ [ B ] C) D) ps) ch))) # </table>
(-> ph (n.E. x (/\ (<-> (n.= (n.+ a c) d) ps) ch))) , (n.= a b)(-> ph (n.E. x (/\ (<-> (n.= (n.+ b c) d) ps) ch)))
ImpReplaceImp1Ex1An1 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ ps [ ch ] ] ] ))) # (-> [ ch ] [ th ] ) # (-> ph (n.E. x (/\ ps [ [ [ th ] ))) # </table>
(-> ph (n.E. x (/\ ps ch))) , (-> ch th)(-> ph (n.E. x (/\ ps th)))
BiReplaceImp1Ex1An1 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ ps [ ch ] ] ] ))) # (<-> [ ch ] [ th ] ) # (-> ph (n.E. x (/\ ps [ [ [ th ] ))) # </table>
(-> ph (n.E. x (/\ ps ch))) , (<-> ch th)(-> ph (n.E. x (/\ ps th)))
NeqReplaceImp1Nex1An1Bi0Neq1Nadd0 # <title> Substitution </title> # <table> # (-> ph (n.E. x (/\ ps (<-> (n.= a (n.+ [ B ] ] ] D)) ch)))) # (n.= [ B ] [ C ] ) # (-> ph (n.E. x (/\ ps (<-> (n.= a (n.+ [ [ [ C ] D)) ch)))) # </table>
(-> ph (n.E. x (/\ ps (<-> (n.= a (n.+ b d)) ch)))) , (n.= b c)(-> ph (n.E. x (/\ ps (<-> (n.= a (n.+ c d)) ch))))
EqReplaceBi0Eq1 # <title> Substitution </title> # <table> # (<-> (= A [ B ] ] ] ) ph) # (= [ B ] [ C ] ) # (<-> (= A [ [ [ C ] ) ph) # </table>
(<-> (= A B) ph) , (= B C)(<-> (= A C) ph)
(-> (n.< (tail A) (head A)) (<-> (= (* B A) (* C A)) (= B C)))
(-> (n.< (head A) (tail A)) (<-> (= (* B A) (* C A)) (= B C)))
BiReplaceImp0Or1 # <title> Substitution </title> # <table> # (-> (\/ ph [ ps ] ] ] ) th) # (<-> [ ps ] [ ch ] ) # (-> (\/ ph [ [ [ ch ] ) th) # </table>
(-> (\/ ph ps) th) , (<-> ps ch)(-> (\/ ph ch) th)
BiReplaceImp0Or0 # <title> Substitution </title> # <table> # (-> (\/ [ ph ] ] ] ch) th) # (<-> [ ph ] [ ps ] ) # (-> (\/ [ [ [ ps ] ch) th) # </table>
(-> (\/ ph ch) th) , (<-> ph ps)(-> (\/ ps ch) th)
mulcan.4 # <title> Multiplication Cancellation </title>
(-> (-. (= A (0))) (<-> (= (* B A) (* C A)) (= B C)))
(-> (-. (= C (0))) (<-> (= (* A C) (* B C)) (= A B)))