let n be non zero Nat; :: thesis: for z1, z2 being Tuple of n, BOOLEAN
for d1, d2 being Element of BOOLEAN holds add_ovfl z1,z2 = (carry (z1 ^ <*d1*>),(z2 ^ <*d2*>)) /. (n + 1)
let z1, z2 be Tuple of n, BOOLEAN ; :: thesis: for d1, d2 being Element of BOOLEAN holds add_ovfl z1,z2 = (carry (z1 ^ <*d1*>),(z2 ^ <*d2*>)) /. (n + 1)
let d1, d2 be Element of BOOLEAN ; :: thesis: add_ovfl z1,z2 = (carry (z1 ^ <*d1*>),(z2 ^ <*d2*>)) /. (n + 1)
A1: ( 1 <= n & n < n + 1 ) by NAT_1:14, XREAL_1:31;
A2: n in Seg n by FINSEQ_1:5;
then A3: z2 /. n = (z2 ^ <*d2*>) /. n by Th2;
( (carry (z1 ^ <*d1*>),(z2 ^ <*d2*>)) /. n = (carry z1,z2) /. n & z1 /. n = (z1 ^ <*d1*>) /. n ) by A2, Th2, Th43;
hence add_ovfl z1,z2 = (carry (z1 ^ <*d1*>),(z2 ^ <*d2*>)) /. (n + 1) by A3, A1, Def5; :: thesis: verum