set n1 = 2;
set n2 = 2;
let am, bm, cm, dm be non pair set ; 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 ; ( 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]
; 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)); 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
; verum