let n be Nat; :: thesis: for ap, bm, cp, dm being FinSequence
for x, y being set holds n -BitFTA1CarryOutput (ap,bm,cp,dm) <> [<*x,y*>,nor2]
let ap, bm, cp, dm be FinSequence; :: thesis: for x, y being set holds n -BitFTA1CarryOutput (ap,bm,cp,dm) <> [<*x,y*>,nor2]
let x, y be set ; :: thesis: n -BitFTA1CarryOutput (ap,bm,cp,dm) <> [<*x,y*>,nor2]
consider h being ManySortedSet of NAT such that
A1: n -BitFTA1CarryOutput (ap,bm,cp,dm) = h . n and
A2: h . 0 = [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] and
A3: for k being Nat holds h . (k + 1) = BitFTA1CarryOutput ((ap . (k + 1)),(bm . (k + 1)),(cp . (k + 1)),(dm . (k + 1)),(h . k)) by Def10;
assume A4: n -BitFTA1CarryOutput (ap,bm,cp,dm) = [<*x,y*>,nor2] ; :: 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 -BitFTA1CarryOutput (ap,bm,cp,dm) = BitFTA1CarryOutput ((ap . (m + 1)),(bm . (m + 1)),(cp . (m + 1)),(dm . (m + 1)),(h . m)) by A1, A3, B1
.= [<*[<*(ap . (m + 1)),(bm . (m + 1))*>,and2c],[<*(bm . (m + 1)),(cp . (m + 1))*>,and2a],[<*(cp . (m + 1)),(ap . (m + 1))*>,and2]*>,or3] ;
then <*x,y*> = <*[<*(ap . (m + 1)),(bm . (m + 1))*>,and2c],[<*(bm . (m + 1)),(cp . (m + 1))*>,and2a],[<*(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;