let ap, bp, cp be non pair set ; :: thesis: for dp, cin being set
for s being State of (BitFTA0Circ (ap,bp,cp,dp,cin))
for k being Nat st k >= 2 holds
(Following (s,k)) . (BitFTA0CarryOutput (ap,bp,cp,dp,cin)) = (Following (s,2)) . (BitFTA0CarryOutput (ap,bp,cp,dp,cin))
let dp, cin be set ; :: thesis: for s being State of (BitFTA0Circ (ap,bp,cp,dp,cin))
for k being Nat st k >= 2 holds
(Following (s,k)) . (BitFTA0CarryOutput (ap,bp,cp,dp,cin)) = (Following (s,2)) . (BitFTA0CarryOutput (ap,bp,cp,dp,cin))
let s be State of (BitFTA0Circ (ap,bp,cp,dp,cin)); :: thesis: for k being Nat st k >= 2 holds
(Following (s,k)) . (BitFTA0CarryOutput (ap,bp,cp,dp,cin)) = (Following (s,2)) . (BitFTA0CarryOutput (ap,bp,cp,dp,cin))
let k be Nat; :: thesis: ( k >= 2 implies (Following (s,k)) . (BitFTA0CarryOutput (ap,bp,cp,dp,cin)) = (Following (s,2)) . (BitFTA0CarryOutput (ap,bp,cp,dp,cin)) )
assume A1: k >= 2 ; :: thesis: (Following (s,k)) . (BitFTA0CarryOutput (ap,bp,cp,dp,cin)) = (Following (s,2)) . (BitFTA0CarryOutput (ap,bp,cp,dp,cin))
set S1 = BitGFA0Str (ap,bp,cp);
set C1 = BitGFA0Circ (ap,bp,cp);
set A1v = GFA0AdderOutput (ap,bp,cp);
set S2 = BitGFA0Str ((GFA0AdderOutput (ap,bp,cp)),cin,dp);
set C2 = BitGFA0Circ ((GFA0AdderOutput (ap,bp,cp)),cin,dp);
set A2v = GFA0CarryOutput (ap,bp,cp);
reconsider s1 = s | the carrier of (BitGFA0Str (ap,bp,cp)) as State of (BitGFA0Circ (ap,bp,cp)) by FACIRC_1:26;
reconsider t = s as State of ((BitGFA0Circ (ap,bp,cp)) +* (BitGFA0Circ ((GFA0AdderOutput (ap,bp,cp)),cin,dp))) ;
A2: InputVertices (BitGFA0Str (ap,bp,cp)) misses InnerVertices (BitGFA0Str ((GFA0AdderOutput (ap,bp,cp)),cin,dp)) by LmT01;
A6: (Following (t,2)) . (GFA0CarryOutput (ap,bp,cp)) = (Following (s1,2)) . (GFA0CarryOutput (ap,bp,cp)) by A2, GFACIRC1:36, FACIRC_1:32;
A7: Following (s1,k) = Following (s1,2) by A1, GFACIRC1:40, CIRCCMB2:4;
thus (Following (s,k)) . (BitFTA0CarryOutput (ap,bp,cp,dp,cin)) = (Following (s,2)) . (BitFTA0CarryOutput (ap,bp,cp,dp,cin)) by A2, GFACIRC1:36, FACIRC_1:32, A6, A7; :: thesis: verum