let n be non empty 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:5;
A3: 1 in Seg 1 by FINSEQ_1:5;
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 9;

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

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

now

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, Th13;

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

now

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

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:45;
hence contradiction by A2, A6, BINARI_2:8; :: thesis: verum

end;

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

then x /. n = TRUE by MARGREL1:45;
hence x = 'not' y by A1, A9, Th22; :: 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:45;
hence contradiction by A2, A6, BINARI_2:8; :: 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 FINSEQ_1:def 18;
then 1 in dom y by A3, FINSEQ_1:def 3;
then A12: y /. 1 = y . 1 by PARTFUN1:def 8
.= 0 by A1, A11, FINSEQ_1:5, FUNCOP_1:13 ;
consider d being Element of BOOLEAN such that
A13: x = <*d*> by A11, FINSEQ_2:117;
A14: d = TRUE by A4, A11, A13, Th11, Th14;

now

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:4, TARSKI:def 1;
hence x /. i = 'not' (y /. i) by A13, A14, A12, FINSEQ_4:25; :: thesis: verum

end;

hence x = 'not' y by BINARITH:def 4; :: 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, Th23
.= 'not' ((Bin1 n) /. n) by A2, BINARITH:def 4
.= 'not' FALSE by A2, A16, BINARI_2:8
.= TRUE ;
len y = n by FINSEQ_1:def 18;
then n in dom y by A2, FINSEQ_1:def 3;
then A18: y /. n = y . n by PARTFUN1:def 8
.= 0 by A1, FINSEQ_1:5, FUNCOP_1:13 ;
A19: x /. n = 'not' (y /. n) by A2, A15, BINARITH:def 4
.= 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 9
.= TRUE by A19, A17 ; :: thesis: verum

end;

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

then len y = 1 by FINSEQ_1:def 18;
then 1 in dom y by A3, FINSEQ_1:def 3;
then A21: y /. 1 = y . 1 by PARTFUN1:def 8
.= 0 by A1, A20, FINSEQ_1:5, FUNCOP_1:13 ;
consider d being Element of BOOLEAN such that
A22: x = <*d*> by A20, FINSEQ_2:117;
d = ('not' y) /. 1 by A15, A22, FINSEQ_4:25
.= 'not' (y /. 1) by A3, A20, BINARITH:def 4
.= TRUE by A21 ;
hence add_ovfl x,(Bin1 n) = TRUE by A20, A22, Th11, Th14; :: thesis: verum

end;

end;