set n1 = 2;
set n2 = 2;
let am, bm, cm, dm be non pair set ; :: thesis: for cin being set st cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2] holds
for s being State of (BitFTA3Circ (am,bm,cm,dm,cin)) holds Following (s,4) is stable
let cin be set ; :: thesis: ( cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2] implies for s being State of (BitFTA3Circ (am,bm,cm,dm,cin)) holds Following (s,4) is stable )
set C = BitFTA3Circ (am,bm,cm,dm,cin);
set S1 = BitGFA3Str (am,bm,cm);
set C1 = BitGFA3Circ (am,bm,cm);
set A1 = GFA3AdderOutput (am,bm,cm);
set S2 = BitGFA3Str ((GFA3AdderOutput (am,bm,cm)),cin,dm);
set C2 = BitGFA3Circ ((GFA3AdderOutput (am,bm,cm)),cin,dm);
set cindm = [<*cin,dm*>,nor2];
set dmA1 = [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2];
assume A1: cin <> [<*dm,(GFA3AdderOutput (am,bm,cm))*>,nor2] ; :: thesis: for s being State of (BitFTA3Circ (am,bm,cm,dm,cin)) holds Following (s,4) is stable
let s be State of (BitFTA3Circ (am,bm,cm,dm,cin)); :: thesis: Following (s,4) is stable
BitGFA3Circ (am,bm,cm) tolerates BitGFA3Circ ((GFA3AdderOutput (am,bm,cm)),cin,dm) by CIRCCOMB:60;
then A2: the Sorts of (BitGFA3Circ (am,bm,cm)) tolerates the Sorts of (BitGFA3Circ ((GFA3AdderOutput (am,bm,cm)),cin,dm)) by CIRCCOMB:def 3;
then reconsider s1 = s | the carrier of (BitGFA3Str (am,bm,cm)) as State of (BitGFA3Circ (am,bm,cm)) by CIRCCOMB:26;
reconsider s2 = (Following (s,2)) | the carrier of (BitGFA3Str ((GFA3AdderOutput (am,bm,cm)),cin,dm)) as State of (BitGFA3Circ ((GFA3AdderOutput (am,bm,cm)),cin,dm)) by A2, CIRCCOMB:26;
A3: ( InputVertices (BitGFA3Str (am,bm,cm)) misses InnerVertices (BitGFA3Str ((GFA3AdderOutput (am,bm,cm)),cin,dm)) & Following (s1,2) is stable ) by Lm32, GFACIRC1:136;
GFA3AdderOutput (am,bm,cm) <> [<*cin,dm*>,nor2] by Lm31;
then Following (s2,2) is stable by A1, GFACIRC1:136;
then Following (s,(2 + 2)) is stable by A3, CIRCCMB2:19, CIRCCOMB:60;
hence Following (s,4) is stable ; :: thesis: verum