let m be non empty Nat; :: thesis: for z being Tuple of m,BOOLEAN
for d being Element of BOOLEAN holds Neg2 (z ^ <*d*>) = (Neg2 z) ^ <*(('not' d) 'xor' (add_ovfl ('not' z),(Bin1 m)))*>
let z be Tuple of m,BOOLEAN ; :: thesis: for d being Element of BOOLEAN holds Neg2 (z ^ <*d*>) = (Neg2 z) ^ <*(('not' d) 'xor' (add_ovfl ('not' z),(Bin1 m)))*>
let d be Element of BOOLEAN ; :: thesis: Neg2 (z ^ <*d*>) = (Neg2 z) ^ <*(('not' d) 'xor' (add_ovfl ('not' z),(Bin1 m)))*>
thus Neg2 (z ^ <*d*>) = (('not' z) ^ <*('not' d)*>) + (Bin1 (m + 1)) by Th11
.= (('not' z) ^ <*('not' d)*>) + ((Bin1 m) ^ <*FALSE *>) by Th9
.= (('not' z) + (Bin1 m)) ^ <*((('not' d) 'xor' FALSE ) 'xor' (add_ovfl ('not' z),(Bin1 m)))*> by BINARITH:45
.= (Neg2 z) ^ <*(('not' d) 'xor' (add_ovfl ('not' z),(Bin1 m)))*> ; :: thesis: verum