let ap, bm, cp be non pair set ; :: thesis: for dm, cin being set
for s being State of (BitFTA1Circ (ap,bm,cp,dm,cin))
for k being Nat st k >= 2 holds
(Following (s,k)) . (BitFTA1CarryOutput (ap,bm,cp,dm,cin)) = (Following (s,2)) . (BitFTA1CarryOutput (ap,bm,cp,dm,cin))
let dm, cin be set ; :: thesis: for s being State of (BitFTA1Circ (ap,bm,cp,dm,cin))
for k being Nat st k >= 2 holds
(Following (s,k)) . (BitFTA1CarryOutput (ap,bm,cp,dm,cin)) = (Following (s,2)) . (BitFTA1CarryOutput (ap,bm,cp,dm,cin))
let s be State of (BitFTA1Circ (ap,bm,cp,dm,cin)); :: thesis: for k being Nat st k >= 2 holds
(Following (s,k)) . (BitFTA1CarryOutput (ap,bm,cp,dm,cin)) = (Following (s,2)) . (BitFTA1CarryOutput (ap,bm,cp,dm,cin))
let k be Nat; :: thesis: ( k >= 2 implies (Following (s,k)) . (BitFTA1CarryOutput (ap,bm,cp,dm,cin)) = (Following (s,2)) . (BitFTA1CarryOutput (ap,bm,cp,dm,cin)) )
assume A1: k >= 2 ; :: thesis: (Following (s,k)) . (BitFTA1CarryOutput (ap,bm,cp,dm,cin)) = (Following (s,2)) . (BitFTA1CarryOutput (ap,bm,cp,dm,cin))
set S1 = BitGFA1Str (ap,bm,cp);
set C1 = BitGFA1Circ (ap,bm,cp);
set A1v = GFA1AdderOutput (ap,bm,cp);
set S2 = BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm);
set C2 = BitGFA2Circ ((GFA1AdderOutput (ap,bm,cp)),cin,dm);
set A2v = GFA1CarryOutput (ap,bm,cp);
reconsider s1 = s | the carrier of (BitGFA1Str (ap,bm,cp)) as State of (BitGFA1Circ (ap,bm,cp)) by FACIRC_1:26;
reconsider t = s as State of ((BitGFA1Circ (ap,bm,cp)) +* (BitGFA2Circ ((GFA1AdderOutput (ap,bm,cp)),cin,dm))) ;
A2: InputVertices (BitGFA1Str (ap,bm,cp)) misses InnerVertices (BitGFA2Str ((GFA1AdderOutput (ap,bm,cp)),cin,dm)) by LmT11;
A5: (Following (t,k)) . (GFA1CarryOutput (ap,bm,cp)) = (Following (s1,k)) . (GFA1CarryOutput (ap,bm,cp)) by A2, GFACIRC1:68, FACIRC_1:32;
A6: (Following (t,2)) . (GFA1CarryOutput (ap,bm,cp)) = (Following (s1,2)) . (GFA1CarryOutput (ap,bm,cp)) by A2, GFACIRC1:68, FACIRC_1:32;
thus (Following (s,k)) . (BitFTA1CarryOutput (ap,bm,cp,dm,cin)) = (Following (s,2)) . (BitFTA1CarryOutput (ap,bm,cp,dm,cin)) by A5, A6, A1, GFACIRC1:72, CIRCCMB2:4; :: thesis: verum