let n be non zero Nat; :: thesis: for x, y being Tuple of n, BOOLEAN st y = 0* n holds
( add_ovfl (x,(Bin1 n)) = TRUE iff x = 'not' y )
let x, y be Tuple of n, BOOLEAN ; :: thesis: ( y = 0* n implies ( add_ovfl (x,(Bin1 n)) = TRUE iff x = 'not' y ) )
assume A1: y = 0* n ; :: thesis: ( add_ovfl (x,(Bin1 n)) = TRUE iff x = 'not' y )
A2: n in Seg n by FINSEQ_1:3;
A3: 1 in Seg 1 by FINSEQ_1:3;
thus ( add_ovfl (x,(Bin1 n)) = TRUE implies x = 'not' y ) :: thesis: ( x = 'not' y implies add_ovfl (x,(Bin1 n)) = TRUE )

proof

assume A4: add_ovfl (x,(Bin1 n)) = TRUE ; :: thesis: x = 'not' y
then A5: (((x /. n) '&' ((Bin1 n) /. n)) 'or' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n))) 'or' (((Bin1 n) /. n) '&' ((carry (x,(Bin1 n))) /. n)) = TRUE by BINARITH:def 6;

per cases ( n <> 1 or n = 1 ) ;

suppose A6: n <> 1 ; :: thesis: x = 'not' y

now :: thesis: x = 'not' y

per cases ( ((x /. n) '&' ((Bin1 n) /. n)) 'or' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n)) = TRUE or ((Bin1 n) /. n) '&' ((carry (x,(Bin1 n))) /. n) = TRUE ) by A5, Th12;

suppose A7: ((x /. n) '&' ((Bin1 n) /. n)) 'or' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n)) = TRUE ; :: thesis: x = 'not' y

now :: thesis: not x <> 'not' y

per cases ( (x /. n) '&' ((Bin1 n) /. n) = TRUE or (x /. n) '&' ((carry (x,(Bin1 n))) /. n) = TRUE ) by A7, Th12;

suppose A8: (x /. n) '&' ((Bin1 n) /. n) = TRUE ; :: thesis: not x <> 'not' y

assume x <> 'not' y ; :: thesis: contradiction
(Bin1 n) /. n = TRUE by A8, MARGREL1:12;
hence contradiction by A2, A6, BINARI_2:6; :: thesis: verum

end;

suppose A9: (x /. n) '&' ((carry (x,(Bin1 n))) /. n) = TRUE ; :: thesis: x = 'not' y

then x /. n = TRUE by MARGREL1:12;
hence x = 'not' y by A1, A9, Th21; :: thesis: verum

end;

end;

end;

hence x = 'not' y ; :: thesis: verum

end;

suppose A10: ((Bin1 n) /. n) '&' ((carry (x,(Bin1 n))) /. n) = TRUE ; :: thesis: not x <> 'not' y

assume x <> 'not' y ; :: thesis: contradiction
(Bin1 n) /. n = TRUE by A10, MARGREL1:12;
hence contradiction by A2, A6, BINARI_2:6; :: thesis: verum

end;

end;

end;

hence x = 'not' y ; :: thesis: verum

end;

suppose A11: n = 1 ; :: thesis: x = 'not' y

then len y = 1 by CARD_1:def 7;
then 1 in dom y by A3, FINSEQ_1:def 3;
then A12: y /. 1 = y . 1 by PARTFUN1:def 6
.= 0 by A1, A11, FINSEQ_1:3, FUNCOP_1:7 ;
consider d being Element of BOOLEAN such that
A13: x = <*d*> by A11, FINSEQ_2:97;
A14: d = TRUE by A4, A11, A13, Th10, Th13;

now :: thesis: for i being Nat st i in Seg n holds
x /. i = 'not' (y /. i)

let i be Nat; :: thesis: ( i in Seg n implies x /. i = 'not' (y /. i) )
assume i in Seg n ; :: thesis: x /. i = 'not' (y /. i)
then i = 1 by A11, FINSEQ_1:2, TARSKI:def 1;
hence x /. i = 'not' (y /. i) by A13, A14, A12, FINSEQ_4:16; :: thesis: verum

end;

hence x = 'not' y by BINARITH:def 1; :: thesis: verum

end;

end;

end;

assume A15: x = 'not' y ; :: thesis: add_ovfl (x,(Bin1 n)) = TRUE

per cases ( n <> 1 or n = 1 ) ;

suppose A16: n <> 1 ; :: thesis: add_ovfl (x,(Bin1 n)) = TRUE

A17: (carry (x,(Bin1 n))) /. n = ('not' (Bin1 n)) /. n by A1, A15, Th22
.= 'not' ((Bin1 n) /. n) by A2, BINARITH:def 1
.= 'not' FALSE by A2, A16, BINARI_2:6
.= TRUE ;
len y = n by CARD_1:def 7;
then n in dom y by A2, FINSEQ_1:def 3;
then A18: y /. n = y . n by PARTFUN1:def 6
.= 0 by A1, FINSEQ_1:3, FUNCOP_1:7 ;
A19: x /. n = 'not' (y /. n) by A2, A15, BINARITH:def 1
.= TRUE by A18 ;
thus add_ovfl (x,(Bin1 n)) = (((x /. n) '&' ((Bin1 n) /. n)) 'or' ((x /. n) '&' ((carry (x,(Bin1 n))) /. n))) 'or' (((Bin1 n) /. n) '&' ((carry (x,(Bin1 n))) /. n)) by BINARITH:def 6
.= TRUE by A19, A17 ; :: thesis: verum

end;

suppose A20: n = 1 ; :: thesis: add_ovfl (x,(Bin1 n)) = TRUE

then len y = 1 by CARD_1:def 7;
then 1 in dom y by A3, FINSEQ_1:def 3;
then A21: y /. 1 = y . 1 by PARTFUN1:def 6
.= 0 by A1, A20, FINSEQ_1:3, FUNCOP_1:7 ;
consider d being Element of BOOLEAN such that
A22: x = <*d*> by A20, FINSEQ_2:97;
d = ('not' y) /. 1 by A15, A22, FINSEQ_4:16
.= 'not' (y /. 1) by A3, A20, BINARITH:def 1
.= TRUE by A21 ;
hence add_ovfl (x,(Bin1 n)) = TRUE by A20, A22, Th10, Th13; :: thesis: verum

end;

end;