let m be non zero Nat; :: thesis: for z1, z2 being Tuple of m, BOOLEAN
for d1, d2 being Element of BOOLEAN holds (z1 ^ <*d1*>) - (z2 ^ <*d2*>) = (z1 + (Neg2 z2)) ^ <*(((d1 'xor' ('not' d2)) 'xor' (add_ovfl (('not' z2),(Bin1 m)))) 'xor' (add_ovfl (z1,(Neg2 z2))))*>
let z1, z2 be Tuple of m, BOOLEAN ; :: thesis: for d1, d2 being Element of BOOLEAN holds (z1 ^ <*d1*>) - (z2 ^ <*d2*>) = (z1 + (Neg2 z2)) ^ <*(((d1 'xor' ('not' d2)) 'xor' (add_ovfl (('not' z2),(Bin1 m)))) 'xor' (add_ovfl (z1,(Neg2 z2))))*>
let d1, d2 be Element of BOOLEAN ; :: thesis: (z1 ^ <*d1*>) - (z2 ^ <*d2*>) = (z1 + (Neg2 z2)) ^ <*(((d1 'xor' ('not' d2)) 'xor' (add_ovfl (('not' z2),(Bin1 m)))) 'xor' (add_ovfl (z1,(Neg2 z2))))*>
thus (z1 ^ <*d1*>) - (z2 ^ <*d2*>) = (z1 ^ <*d1*>) + (Neg2 (z2 ^ <*d2*>)) by Th17
.= (z1 ^ <*d1*>) + ((Neg2 z2) ^ <*(('not' d2) 'xor' (add_ovfl (('not' z2),(Bin1 m))))*>) by Th14
.= (z1 + (Neg2 z2)) ^ <*((d1 'xor' (('not' d2) 'xor' (add_ovfl (('not' z2),(Bin1 m))))) 'xor' (add_ovfl (z1,(Neg2 z2))))*> by BINARITH:19
.= (z1 + (Neg2 z2)) ^ <*(((d1 'xor' ('not' d2)) 'xor' (add_ovfl (('not' z2),(Bin1 m)))) 'xor' (add_ovfl (z1,(Neg2 z2))))*> by XBOOLEAN:73 ; :: thesis: verum