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)))
mulcan.1
(<-> (= (* 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)
mulcan.2
(-> (n.< (tail A) (head A)) (<-> (= (* B A) (* C A)) (= B C)))
mulcan.3
(-> (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)))
mulcan
(-> (-. (= C (0))) (<-> (= (* A C) (* B C)) (= A B)))
