let n be non zero Nat; :: thesis: for z1, z2 being Tuple of n, BOOLEAN
for d1, d2 being Element of BOOLEAN holds (z1 ^ <*d1*>) + (z2 ^ <*d2*>) = (z1 + z2) ^ <*((d1 'xor' d2) 'xor' (add_ovfl (z1,z2)))*>
let z1, z2 be Tuple of n, BOOLEAN ; :: thesis: for d1, d2 being Element of BOOLEAN holds (z1 ^ <*d1*>) + (z2 ^ <*d2*>) = (z1 + z2) ^ <*((d1 'xor' d2) 'xor' (add_ovfl (z1,z2)))*>
let d1, d2 be Element of BOOLEAN ; :: thesis: (z1 ^ <*d1*>) + (z2 ^ <*d2*>) = (z1 + z2) ^ <*((d1 'xor' d2) 'xor' (add_ovfl (z1,z2)))*>
for i being Nat st i in Seg (n + 1) holds
((z1 + z2) ^ <*((d1 'xor' d2) 'xor' (add_ovfl (z1,z2)))*>) /. i = (((z1 ^ <*d1*>) /. i) 'xor' ((z2 ^ <*d2*>) /. i)) 'xor' ((carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i)

proof

A1: Seg (n + 1) = (Seg n) \/ {.(n + 1).} by FINSEQ_1:9;
let i be Nat; :: thesis: ( i in Seg (n + 1) implies ((z1 + z2) ^ <*((d1 'xor' d2) 'xor' (add_ovfl (z1,z2)))*>) /. i = (((z1 ^ <*d1*>) /. i) 'xor' ((z2 ^ <*d2*>) /. i)) 'xor' ((carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i) )
assume A2: i in Seg (n + 1) ; :: thesis: ((z1 + z2) ^ <*((d1 'xor' d2) 'xor' (add_ovfl (z1,z2)))*>) /. i = (((z1 ^ <*d1*>) /. i) 'xor' ((z2 ^ <*d2*>) /. i)) 'xor' ((carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i)

per cases ( i in Seg n or i in {.(n + 1).} ) by A2, A1, XBOOLE_0:def 3;

suppose A3: i in Seg n ; :: thesis: ((z1 + z2) ^ <*((d1 'xor' d2) 'xor' (add_ovfl (z1,z2)))*>) /. i = (((z1 ^ <*d1*>) /. i) 'xor' ((z2 ^ <*d2*>) /. i)) 'xor' ((carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i)

hence ((z1 + z2) ^ <*((d1 'xor' d2) 'xor' (add_ovfl (z1,z2)))*>) /. i = (z1 + z2) /. i by Th1
.= ((z1 /. i) 'xor' (z2 /. i)) 'xor' ((carry (z1,z2)) /. i) by A3, Def5
.= (((z1 ^ <*d1*>) /. i) 'xor' (z2 /. i)) 'xor' ((carry (z1,z2)) /. i) by A3, Th1
.= (((z1 ^ <*d1*>) /. i) 'xor' ((z2 ^ <*d2*>) /. i)) 'xor' ((carry (z1,z2)) /. i) by A3, Th1
.= (((z1 ^ <*d1*>) /. i) 'xor' ((z2 ^ <*d2*>) /. i)) 'xor' ((carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i) by A3, Th17 ;
:: thesis: verum

end;

suppose i in {.(n + 1).} ; :: thesis: ((z1 + z2) ^ <*((d1 'xor' d2) 'xor' (add_ovfl (z1,z2)))*>) /. i = (((z1 ^ <*d1*>) /. i) 'xor' ((z2 ^ <*d2*>) /. i)) 'xor' ((carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i)

then A4: i = n + 1 by TARSKI:def 1;
hence ((z1 + z2) ^ <*((d1 'xor' d2) 'xor' (add_ovfl (z1,z2)))*>) /. i = (d1 'xor' d2) 'xor' (add_ovfl (z1,z2)) by Th2
.= (d1 'xor' d2) 'xor' ((carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i) by A4, Th18
.= (d1 'xor' ((z2 ^ <*d2*>) /. i)) 'xor' ((carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i) by A4, Th2
.= (((z1 ^ <*d1*>) /. i) 'xor' ((z2 ^ <*d2*>) /. i)) 'xor' ((carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i) by A4, Th2 ;
:: thesis: verum

end;

end;

end;

hence (z1 ^ <*d1*>) + (z2 ^ <*d2*>) = (z1 + z2) ^ <*((d1 'xor' d2) 'xor' (add_ovfl (z1,z2)))*> by Def5; :: thesis: verum