let n be non zero Nat; :: thesis: 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 ; :: thesis: 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 ; :: thesis: 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 );
A1:
S1[1]
A2:
for i being non empty Nat st S1[i] holds
S1[i + 1]
proof
let i be non
empty Nat;
:: thesis: ( S1[i] implies S1[i + 1] )
assume A3:
S1[
i]
;
:: thesis: S1[i + 1]
A4:
i + 1
> i
by XREAL_1:31;
assume
i + 1
in Seg n
;
:: thesis: (carry (z1 ^ <*d1*>),(z2 ^ <*d2*>)) /. (i + 1) = (carry z1,z2) /. (i + 1)
then
(
i + 1
>= 1 &
i + 1
<= n )
by FINSEQ_1:3;
then A5:
( 1
<= i &
i < n )
by A4, NAT_1:14, XXREAL_0:2;
then A6:
i in Seg n
by FINSEQ_1:3;
then A7:
(z1 ^ <*d1*>) /. i = z1 /. i
by Th2;
A8:
(z2 ^ <*d2*>) /. i = z2 /. i
by A6, Th2;
n <= n + 1
by NAT_1:11;
then
( 1
<= i &
i < n + 1 )
by A5, XXREAL_0:2;
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 A3, A7, A8, Def5, A5, FINSEQ_1:3
.=
(carry z1,z2) /. (i + 1)
by A5, Def5
;
:: thesis: verum
end;
let i be Nat; :: thesis: ( i in Seg n implies (carry (z1 ^ <*d1*>),(z2 ^ <*d2*>)) /. i = (carry z1,z2) /. i )
assume A9:
i in Seg n
; :: thesis: (carry (z1 ^ <*d1*>),(z2 ^ <*d2*>)) /. i = (carry z1,z2) /. i
then A10:
not i is empty
by FINSEQ_1:3;
for i being non empty Nat holds S1[i]
from NAT_1:sch 10(A1, A2);
hence
(carry (z1 ^ <*d1*>),(z2 ^ <*d2*>)) /. i = (carry z1,z2) /. i
by A9, A10; :: thesis: verum