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 (x /. n) '&' ((Bin1 n) /. n) = TRUE ; :: thesis: not x <> 'not' y

then A8: ( x /. n = TRUE & (Bin1 n) /. n = TRUE ) by MARGREL1:45;
assume x <> 'not' y ; :: thesis: contradiction
thus contradiction by A2, A6, A8, BINARI_2:8; :: thesis: verum

end;

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

then ( x /. n = TRUE & (carry x,(Bin1 n)) /. n = TRUE ) by MARGREL1:45;
hence x = 'not' y by A1, Th22; :: thesis: verum

end;

end;

end;

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

end;

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

then A9: ( (Bin1 n) /. n = TRUE & (carry x,(Bin1 n)) /. n = TRUE ) by MARGREL1:45;
assume x <> 'not' y ; :: thesis: contradiction
thus contradiction by A2, A6, A9, BINARI_2:8; :: thesis: verum

end;

end;

end;

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

end;

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

then consider d being Element of BOOLEAN such that
A11: x = <*d*> by FINSEQ_2:117;
A12: d = TRUE by A4, A10, A11, Th11, Th14;
len y = 1 by A10, FINSEQ_1:def 18;
then 1 in dom y by A3, FINSEQ_1:def 3;
then A13: y /. 1 = y . 1 by PARTFUN1:def 8
.= 0 by A1, A10, FINSEQ_1:5, FUNCOP_1:13 ;

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

end;

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

end;

end;

end;

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

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

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

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

end;

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

then consider d being Element of BOOLEAN such that
A20: x = <*d*> by FINSEQ_2:117;
len y = 1 by A19, 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, A19, FINSEQ_1:5, FUNCOP_1:13 ;
d = ('not' y) /. 1 by A14, A20, FINSEQ_4:25
.= 'not' (y /. 1) by A3, A19, BINARITH:def 4
.= TRUE by A21 ;
hence add_ovfl x,(Bin1 n) = TRUE by A19, A20, Th11, Th14; :: thesis: verum

end;

end;