let n be Nat; :: thesis: for ap, bp, cp, dp being FinSequence
for x, y being set holds n -BitFTA0CarryOutput (ap,bp,cp,dp) <> [<*x,y*>,and2]
let ap, bp, cp, dp be FinSequence; :: thesis: for x, y being set holds n -BitFTA0CarryOutput (ap,bp,cp,dp) <> [<*x,y*>,and2]
let x, y be set ; :: thesis: n -BitFTA0CarryOutput (ap,bp,cp,dp) <> [<*x,y*>,and2]
consider h being ManySortedSet of NAT such that
A1: n -BitFTA0CarryOutput (ap,bp,cp,dp) = h . n and
A2: h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] and
A3: for k being Nat holds h . (k + 1) = BitFTA0CarryOutput ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)),(dp . (k + 1)),(h . k)) by Def3;
assume A4: n -BitFTA0CarryOutput (ap,bp,cp,dp) = [<*x,y*>,and2] ; :: thesis: contradiction

per cases ( n = 0 or ex m being Nat st n = m + 1 ) by NAT_1:6;

suppose n = 0 ; :: thesis: contradiction

hence contradiction by XTUPLE_0:1, A1, A2, A4; :: thesis: verum

end;

suppose ex m being Nat st n = m + 1 ; :: thesis: contradiction

then consider m being Nat such that
B1: n = m + 1 ;
n -BitFTA0CarryOutput (ap,bp,cp,dp) = BitFTA0CarryOutput ((ap . (m + 1)),(bp . (m + 1)),(cp . (m + 1)),(dp . (m + 1)),(h . m)) by A1, A3, B1
.= [<*[<*(ap . (m + 1)),(bp . (m + 1))*>,and2],[<*(bp . (m + 1)),(cp . (m + 1))*>,and2],[<*(cp . (m + 1)),(ap . (m + 1))*>,and2]*>,or3] ;
then <*x,y*> = <*[<*(ap . (m + 1)),(bp . (m + 1))*>,and2],[<*(bp . (m + 1)),(cp . (m + 1))*>,and2],[<*(cp . (m + 1)),(ap . (m + 1))*>,and2]*> by XTUPLE_0:1, A4;
then len <*x,y*> = 3 by FINSEQ_1:45;
hence contradiction by FINSEQ_1:44; :: thesis: verum

end;

end;