set f1 = and2a ;
set f2 = and2c ;
set f3 = nor2 ;
set f0 = xor2c ;
let x, y, z be set ; ( z <> [<*x,y*>,xor2c] & x <> [<*y,z*>,and2c] & y <> [<*z,x*>,nor2] & z <> [<*x,y*>,and2a] implies for s being State of (BitGFA2Circ (x,y,z)) holds Following (s,2) is stable )
assume that
A1:
z <> [<*x,y*>,xor2c]
and
A2:
( x <> [<*y,z*>,and2c] & y <> [<*z,x*>,nor2] & z <> [<*x,y*>,and2a] )
; for s being State of (BitGFA2Circ (x,y,z)) holds Following (s,2) is stable
set A = BitGFA2Circ (x,y,z);
let s be State of (BitGFA2Circ (x,y,z)); Following (s,2) is stable
set S2 = GFA2CarryStr (x,y,z);
set S1 = GFA2AdderStr (x,y,z);
InputVertices (GFA2AdderStr (x,y,z)) = {x,y,z}
by A1, FACIRC_1:57;
then A3:
InputVertices (GFA2AdderStr (x,y,z)) = InputVertices (GFA2CarryStr (x,y,z))
by A2, Th77;
set A1 = GFA2AdderCirc (x,y,z);
reconsider s1 = s | the carrier of (GFA2AdderStr (x,y,z)) as State of (GFA2AdderCirc (x,y,z)) by FACIRC_1:26;
Following (s1,2) is stable
by A1, FACIRC_1:63;
then A4: Following (s1,2) =
Following (Following (s1,2))
.=
Following (s1,(2 + 1))
by FACIRC_1:12
;
set A2 = GFA2CarryCirc (x,y,z);
reconsider s2 = s | the carrier of (GFA2CarryStr (x,y,z)) as State of (GFA2CarryCirc (x,y,z)) by FACIRC_1:26;
Following (s2,2) is stable
by A2, Th86;
then A5: Following (s2,2) =
Following (Following (s2,2))
.=
Following (s2,(2 + 1))
by FACIRC_1:12
;
reconsider t = s as State of ((GFA2AdderCirc (x,y,z)) +* (GFA2CarryCirc (x,y,z))) ;
set S = BitGFA2Str (x,y,z);
A6:
dom (Following (s,3)) = the carrier of (BitGFA2Str (x,y,z))
by CIRCUIT1:3;
InnerVertices (GFA2CarryStr (x,y,z)) misses InputVertices (GFA2CarryStr (x,y,z))
by XBOOLE_1:79;
then A7:
( Following (s1,2) = (Following (t,2)) | the carrier of (GFA2AdderStr (x,y,z)) & Following (s1,3) = (Following (t,3)) | the carrier of (GFA2AdderStr (x,y,z)) )
by A3, FACIRC_1:30;
InnerVertices (GFA2AdderStr (x,y,z)) misses InputVertices (GFA2AdderStr (x,y,z))
by XBOOLE_1:79;
then A8:
( Following (s2,2) = (Following (t,2)) | the carrier of (GFA2CarryStr (x,y,z)) & Following (s2,3) = (Following (t,3)) | the carrier of (GFA2CarryStr (x,y,z)) )
by A3, FACIRC_1:31;
A9:
the carrier of (BitGFA2Str (x,y,z)) = the carrier of (GFA2AdderStr (x,y,z)) \/ the carrier of (GFA2CarryStr (x,y,z))
by CIRCCOMB:def 2;
A10:
( dom (Following (s1,2)) = the carrier of (GFA2AdderStr (x,y,z)) & dom (Following (s2,2)) = the carrier of (GFA2CarryStr (x,y,z)) )
by CIRCUIT1:3;
A11:
now for a being object st a in the carrier of (BitGFA2Str (x,y,z)) holds
(Following (s,2)) . a = (Following (Following (s,2))) . alet a be
object ;
( a in the carrier of (BitGFA2Str (x,y,z)) implies (Following (s,2)) . a = (Following (Following (s,2))) . a )assume
a in the
carrier of
(BitGFA2Str (x,y,z))
;
(Following (s,2)) . a = (Following (Following (s,2))) . athen
(
a in the
carrier of
(GFA2AdderStr (x,y,z)) or
a in the
carrier of
(GFA2CarryStr (x,y,z)) )
by A9, XBOOLE_0:def 3;
then
( (
(Following (s,2)) . a = (Following (s1,2)) . a &
(Following (s,3)) . a = (Following (s1,3)) . a ) or (
(Following (s,2)) . a = (Following (s2,2)) . a &
(Following (s,3)) . a = (Following (s2,3)) . a ) )
by A7, A8, A4, A5, A10, FUNCT_1:47;
hence
(Following (s,2)) . a = (Following (Following (s,2))) . a
by A4, A5, FACIRC_1:12;
verum end;
( Following (s,(2 + 1)) = Following (Following (s,2)) & dom (Following (s,2)) = the carrier of (BitGFA2Str (x,y,z)) )
by CIRCUIT1:3, FACIRC_1:12;
hence
Following (s,2) = Following (Following (s,2))
by A6, A11, FUNCT_1:2; CIRCUIT2:def 6 verum