let m be non zero 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 Th9
.= (('not' z) ^ <*('not' d)*>) + ((Bin1 m) ^ <*FALSE*>) by Th7
.= (('not' z) + (Bin1 m)) ^ <*((('not' d) 'xor' FALSE) 'xor' (add_ovfl (('not' z),(Bin1 m))))*> by BINARITH:19
.= (Neg2 z) ^ <*(('not' d) 'xor' (add_ovfl (('not' z),(Bin1 m))))*> ; :: thesis: verum