add432 Show Code edit
## Rearrange Addition Terms
thm (add432 () () (= (+ (+ A B) (+ C D)) (+ (+ A D) (+ B C)))
## <d 'Associative Property '>
A B (+ C D) addass
(= (+ (+ A B) (+ C D)) (+ A (+ B (+ C D))))
## </d 'Associative Property '>
## <d 'Associative Property '>
B C D addass
(= (+ (+ B C) D) (+ B (+ C D)))
## <d 'Commutative Property'>
(+ (+ B C) D) (+ B (+ C D)) eqcom
(<-> (= (+ (+ B C) D) (+ B (+ C D))) (= (+ B (+ C D)) (+ (+ B C) D)))
mpbi
(= (+ B (+ C D)) (+ (+ B C) D))
## </d 'Commutative Property'>
EqReplaceEq1Add1
(= (+ (+ A B) (+ C D)) (+ A (+ (+ B C) D)))
## </d 'Associative Property '>
## <d 'Commutative Property of Addition '>
(+ B C) D addcom
(= (+ (+ B C) D) (+ D (+ B C)))
EqReplaceEq1Add1
(= (+ (+ A B) (+ C D)) (+ A (+ D (+ B C))))
## </d 'Commutative Property of Addition '>
## <d 'Associative Property '>
A D (+ B C) addass
(= (+ (+ A D) (+ B C)) (+ A (+ D (+ B C))))
## <d 'Commutative Property'>
(+ (+ A D) (+ B C)) (+ A (+ D (+ B C))) eqcom
(<-> (= (+ (+ A D) (+ B C)) (+ A (+ D (+ B C)))) (= (+ A (+ D (+ B C))) (+ (+ A D) (+ B C))))
mpbi
(= (+ A (+ D (+ B C))) (+ (+ A D) (+ B C)))
## </d 'Commutative Property'>
EqReplaceEq1
(= (+ (+ A B) (+ C D)) (+ (+ A D) (+ B C)))
## </d 'Associative Property '>
)
edit