let K be non zero Nat; :: thesis: for x, y being Tuple of K, BOOLEAN st y = 0* K holds
for n being non zero Nat st n <= K holds
( (carry (x,y)) /. n = 0 & (carry (y,x)) /. n = 0 )
let x, y be Tuple of K, BOOLEAN ; :: thesis: ( y = 0* K implies for n being non zero Nat st n <= K holds
( (carry (x,y)) /. n = 0 & (carry (y,x)) /. n = 0 ) )
assume AS: y = 0* K ; :: thesis: for n being non zero Nat st n <= K holds
( (carry (x,y)) /. n = 0 & (carry (y,x)) /. n = 0 )
defpred S1[ Nat] means ( 1 <= $1 & $1 <= K implies (carry (x,y)) /. $1 = 0 );
P1: S1[1] by BINARITH:def 2;
P2: for i being non zero Nat st S1[i] holds
S1[i + 1]
proof
let i be non zero Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A2: S1[i] ; :: thesis: S1[i + 1]
assume ( 1 <= i + 1 & i + 1 <= K ) ; :: thesis: (carry (x,y)) /. (i + 1) = 0
then A4: ( 1 <= i & i < K ) by NAT_1:25, XXREAL_0:2, NAT_1:16;
hence (carry (x,y)) /. (i + 1) = (((x /. i) '&' (y /. i)) 'or' ((x /. i) '&' ((carry (x,y)) /. i))) 'or' ((y /. i) '&' ((carry (x,y)) /. i)) by BINARITH:def 2
.= 0 by A4, A2, AS, LMExtBit4 ;
:: thesis: verum
end;
P3: for k being non zero Nat holds S1[k] from NAT_1:sch 10(P1, P2);
 let n be non zero Nat; :: thesis: ( n <= K implies ( (carry (x,y)) /. n = 0 & (carry (y,x)) /. n = 0 ) )
assume n <= K ; :: thesis: ( (carry (x,y)) /. n = 0 & (carry (y,x)) /. n = 0 )
then ( 1 <= n & n <= K ) by NAT_1:25;
hence (carry (x,y)) /. n = 0 by P3; :: thesis: (carry (y,x)) /. n = 0
hence (carry (y,x)) /. n = 0 by LMExtBit501; :: thesis: verum