let n be non zero Nat; for z1, z2 being Tuple of n, BOOLEAN
for d1, d2 being Element of BOOLEAN
for i being Nat st i in Seg n holds
(carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i = (carry (z1,z2)) /. i
let z1, z2 be Tuple of n, BOOLEAN ; for d1, d2 being Element of BOOLEAN
for i being Nat st i in Seg n holds
(carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i = (carry (z1,z2)) /. i
let d1, d2 be Element of BOOLEAN ; for i being Nat st i in Seg n holds
(carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i = (carry (z1,z2)) /. i
defpred S1[ Nat] means ( $1 in Seg n implies (carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. $1 = (carry (z1,z2)) /. $1 );
let i be Nat; ( i in Seg n implies (carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i = (carry (z1,z2)) /. i )
A1:
for i being non zero Nat st S1[i] holds
S1[i + 1]
proof
let i be non
zero Nat;
( S1[i] implies S1[i + 1] )
assume A2:
S1[
i]
;
S1[i + 1]
assume
i + 1
in Seg n
;
(carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (i + 1) = (carry (z1,z2)) /. (i + 1)
then
(
i + 1
> i &
i + 1
<= n )
by FINSEQ_1:1, XREAL_1:29;
then A3:
i < n
by XXREAL_0:2;
n <= n + 1
by NAT_1:11;
then A4:
i < n + 1
by A3, XXREAL_0:2;
A5:
1
<= i
by NAT_1:14;
then
i in Seg n
by A3;
then
(
(z1 ^ <*d1*>) /. i = z1 /. i &
(z2 ^ <*d2*>) /. i = z2 /. i )
by Th1;
hence (carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. (i + 1) =
(((z1 /. i) '&' (z2 /. i)) 'or' ((z1 /. i) '&' ((carry (z1,z2)) /. i))) 'or' ((z2 /. i) '&' ((carry (z1,z2)) /. i))
by A2, A5, A3, A4, Def2
.=
(carry (z1,z2)) /. (i + 1)
by A5, A3, Def2
;
verum
end;
A6:
S1[1]
A7:
for i being non zero Nat holds S1[i]
from NAT_1:sch 10(A6, A1);
assume A8:
i in Seg n
; (carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i = (carry (z1,z2)) /. i
then
not i is zero
by FINSEQ_1:1;
hence
(carry ((z1 ^ <*d1*>),(z2 ^ <*d2*>))) /. i = (carry (z1,z2)) /. i
by A8, A7; verum