let K be non zero Nat; :: thesis: for x, y being Tuple of K, BOOLEAN
for x1, y1 being Tuple of K + 1, BOOLEAN st not x,y are_summable & x1 = x ^ <*0*> & y1 = y ^ <*0*> holds
(x1 + y1) . (len (x1 + y1)) = 1
let x, y be Tuple of K, BOOLEAN ; :: thesis: for x1, y1 being Tuple of K + 1, BOOLEAN st not x,y are_summable & x1 = x ^ <*0*> & y1 = y ^ <*0*> holds
(x1 + y1) . (len (x1 + y1)) = 1
let x1, y1 be Tuple of K + 1, BOOLEAN ; :: thesis: ( not x,y are_summable & x1 = x ^ <*0*> & y1 = y ^ <*0*> implies (x1 + y1) . (len (x1 + y1)) = 1 )
assume AS: ( not x,y are_summable & x1 = x ^ <*0*> & y1 = y ^ <*0*> ) ; :: thesis: (x1 + y1) . (len (x1 + y1)) = 1
then X0: not add_ovfl (x,y) = 0 by BINARITH:def 7;
PX1: add_ovfl (x,y) = 1 by X0, MARGREL1:def 11, TARSKI:def 2;
then X1: (((x /. K) '&' (y /. K)) 'or' ((x /. K) '&' ((carry (x,y)) /. K))) 'or' ((y /. K) '&' ((carry (x,y)) /. K)) = 1 by BINARITH:def 6;
set K1 = K + 1;
X3: ( len x = K & len y = K ) by CARD_1:def 7;
then XX3: ( len x in Seg K & len y in Seg K ) by FINSEQ_1:3;
L0: len y1 = K + 1 by CARD_1:def 7;
1 <= len y1 by NAT_1:25;
then len y1 in dom y1 by FINSEQ_3:25;
then L2: y1 /. (len y1) = y1 . (len y1) by PARTFUN1:def 6
.= 0 by L0, AS, FINSEQ_1:42, X3 ;
R0: len x1 = K + 1 by CARD_1:def 7;
1 <= len x1 by NAT_1:25;
then len x1 in dom x1 by FINSEQ_3:25;
then R2: x1 /. (len x1) = x1 . (len x1) by PARTFUN1:def 6
.= 0 by R0, AS, FINSEQ_1:42, X3 ;
P2: len (x1 + y1) = K + 1 by CARD_1:def 7;
1 <= len (x1 + y1) by NAT_1:25;
then P3: len (x1 + y1) in Seg (K + 1) by P2, FINSEQ_1:1;
then PP5: len (x1 + y1) in dom (x1 + y1) by P2, FINSEQ_1:def 3;
A1: ( (carry (x,y)) /. 1 = FALSE & ( for i being Nat st 1 <= i & i < K holds
(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;
XR0: len (carry (x,y)) = K by CARD_1:def 7;
1 <= len (carry (x,y)) by NAT_1:25;
then PXR1: len (carry (x,y)) in Seg K by XR0, FINSEQ_1:1;
reconsider i1 = 1 as Element of BOOLEAN by MARGREL1:def 11, TARSKI:def 2;
reconsider Z1 = <*i1*> as FinSequence of BOOLEAN ;
len Z1 = 1 by FINSEQ_1:40;
then reconsider Z1 = <*1*> as Tuple of 1, BOOLEAN ;
(carry (x,y)) ^ Z1 is Tuple of K + 1, BOOLEAN ;
then reconsider S = (carry (x,y)) ^ <*1*> as Tuple of K + 1, BOOLEAN ;
reconsider i0 = 0 as Element of BOOLEAN by MARGREL1:def 11, TARSKI:def 2;
reconsider Z0 = <*i0*> as FinSequence of BOOLEAN ;
len Z0 = 1 by FINSEQ_1:40;
then reconsider Z0 = <*0*> as Tuple of 1, BOOLEAN ;
TT1: S = (carry (x,y)) ^ Z1 ;
TT2: x1 = x ^ Z0 by AS;
TT3: y1 = y ^ Z0 by AS;
A20: S /. 1 = FALSE

proof

1 <= K by NAT_1:25;
then 1 in Seg K by FINSEQ_1:1;
then 1 in dom (carry (x,y)) by XR0, FINSEQ_1:def 3;
hence S /. 1 = FALSE by A1, TT1, FINSEQ_4:68; :: thesis: verum

end;

K in dom x by XX3, X3, FINSEQ_1:def 3;
then T3: x1 /. K = x /. K by TT2, FINSEQ_4:68;
K in dom y by XX3, X3, FINSEQ_1:def 3;
then T4: y1 /. K = y /. K by TT3, FINSEQ_4:68;
K in dom (carry (x,y)) by PXR1, XR0, FINSEQ_1:def 3;
then T2: S /. K = (carry (x,y)) /. K by TT1, FINSEQ_4:68;
A2: for i being Nat st 1 <= i & i < K + 1 holds
S /. (i + 1) = (((x1 /. i) '&' (y1 /. i)) 'or' ((x1 /. i) '&' (S /. i))) 'or' ((y1 /. i) '&' (S /. i))

proof

let i be Nat; :: thesis: ( 1 <= i & i < K + 1 implies S /. (i + 1) = (((x1 /. i) '&' (y1 /. i)) 'or' ((x1 /. i) '&' (S /. i))) 'or' ((y1 /. i) '&' (S /. i)) )
assume AS11: ( 1 <= i & i < K + 1 ) ; :: thesis: S /. (i + 1) = (((x1 /. i) '&' (y1 /. i)) 'or' ((x1 /. i) '&' (S /. i))) 'or' ((y1 /. i) '&' (S /. i))

per cases ( not i < K or i < K ) ;

suppose SXX1: not i < K ; :: thesis: S /. (i + 1) = (((x1 /. i) '&' (y1 /. i)) 'or' ((x1 /. i) '&' (S /. i))) 'or' ((y1 /. i) '&' (S /. i))

i <= K by NAT_1:13, AS11;
then XX: i = K by SXX1, XXREAL_0:1;
then S /. (i + 1) = i1 by FINSEQ_4:67, XR0
.= 1 ;
hence S /. (i + 1) = (((x1 /. i) '&' (y1 /. i)) 'or' ((x1 /. i) '&' (S /. i))) 'or' ((y1 /. i) '&' (S /. i)) by PX1, XX, T2, T3, T4, BINARITH:def 6; :: thesis: verum

end;

suppose C1: i < K ; :: thesis: S /. (i + 1) = (((x1 /. i) '&' (y1 /. i)) 'or' ((x1 /. i) '&' (S /. i))) 'or' ((y1 /. i) '&' (S /. i))

then C2: i in Seg K by AS11, FINSEQ_1:1;
then i in dom (carry (x,y)) by XR0, FINSEQ_1:def 3;
then T2: S /. i = (carry (x,y)) /. i by TT1, FINSEQ_4:68;
i in dom x by C2, X3, FINSEQ_1:def 3;
then T3: x1 /. i = x /. i by TT2, FINSEQ_4:68;
i in dom y by C2, X3, FINSEQ_1:def 3;
then T4: y1 /. i = y /. i by TT3, FINSEQ_4:68;
T5: i + 1 <= K by C1, NAT_1:13;
1 + 0 <= i + 1 by XREAL_1:7;
then i + 1 in Seg K by T5, FINSEQ_1:1;
then i + 1 in dom (carry (x,y)) by XR0, FINSEQ_1:def 3;
hence S /. (i + 1) = (carry (x,y)) /. (i + 1) by TT1, FINSEQ_4:68
.= (((x1 /. i) '&' (y1 /. i)) 'or' ((x1 /. i) '&' (S /. i))) 'or' ((y1 /. i) '&' (S /. i)) by T2, T3, T4, C1, AS11, BINARITH:def 2 ;
:: thesis: verum

end;

end;

end;

then T1: S = carry (x1,y1) by A20, BINARITH:def 2;
K in dom (carry (x,y)) by PXR1, XR0, FINSEQ_1:def 3;
then T2: S /. K = (carry (x,y)) /. K by TT1, FINSEQ_4:68;
T6: len (x1 + y1) = K + 1 by CARD_1:def 7;
X2: 1 <= K by NAT_1:25;
(x1 + y1) /. (len (x1 + y1)) = ((x1 /. (len (x1 + y1))) 'xor' (y1 /. (len (x1 + y1)))) 'xor' ((carry (x1,y1)) /. (len (x1 + y1))) by BINARITH:def 5, P3
.= 1 by R2, R0, L2, L0, X2, T1, T6, NAT_1:16, X1, T2, T3, T4, A2 ;
hence (x1 + y1) . (len (x1 + y1)) = 1 by PP5, PARTFUN1:def 6; :: thesis: verum