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:29;
A2: n in Seg n by FINSEQ_1:3;
then A3: z2 /. n = (z2 ^ <*d2*>) /. n by Th1;
( (carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. n = (carry (z1,z2)) /. n & z1 /. n = (z1 ^ <*d1*>) /. n ) by A2, Th1, Th17;
hence add_ovfl (z1,z2) = (carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (n + 1) by A3, A1, Def2; :: thesis: verum