set f1 = and2 ;
set f2 = and2 ;
set f3 = and2 ;
set f0 = xor2 ;
let x, y, z be set ; ( z <> [<*x,y*>,xor2] & x <> [<*y,z*>,and2] & y <> [<*z,x*>,and2] & z <> [<*x,y*>,and2] implies for s being State of (BitGFA0Circ (x,y,z)) holds Following (s,2) is stable )
assume that
A1:
z <> [<*x,y*>,xor2]
and
A2:
( x <> [<*y,z*>,and2] & y <> [<*z,x*>,and2] & z <> [<*x,y*>,and2] )
; for s being State of (BitGFA0Circ (x,y,z)) holds Following (s,2) is stable
set A = BitGFA0Circ (x,y,z);
let s be State of (BitGFA0Circ (x,y,z)); Following (s,2) is stable
set S2 = GFA0CarryStr (x,y,z);
set S1 = GFA0AdderStr (x,y,z);
InputVertices (GFA0AdderStr (x,y,z)) = {x,y,z}
by A1, FACIRC_1:57;
then A3:
InputVertices (GFA0AdderStr (x,y,z)) = InputVertices (GFA0CarryStr (x,y,z))
by A2, Th14;
set A1 = GFA0AdderCirc (x,y,z);
reconsider s1 = s | the carrier of (GFA0AdderStr (x,y,z)) as State of (GFA0AdderCirc (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 = GFA0CarryCirc (x,y,z);
reconsider s2 = s | the carrier of (GFA0CarryStr (x,y,z)) as State of (GFA0CarryCirc (x,y,z)) by FACIRC_1:26;
Following (s2,2) is stable
by A2, Th23;
then A5: Following (s2,2) =
Following (Following (s2,2))
.=
Following (s2,(2 + 1))
by FACIRC_1:12
;
reconsider t = s as State of ((GFA0AdderCirc (x,y,z)) +* (GFA0CarryCirc (x,y,z))) ;
set S = BitGFA0Str (x,y,z);
A6:
dom (Following (s,3)) = the carrier of (BitGFA0Str (x,y,z))
by CIRCUIT1:3;
InnerVertices (GFA0CarryStr (x,y,z)) misses InputVertices (GFA0CarryStr (x,y,z))
by XBOOLE_1:79;
then A7:
( Following (s1,2) = (Following (t,2)) | the carrier of (GFA0AdderStr (x,y,z)) & Following (s1,3) = (Following (t,3)) | the carrier of (GFA0AdderStr (x,y,z)) )
by A3, FACIRC_1:30;
InnerVertices (GFA0AdderStr (x,y,z)) misses InputVertices (GFA0AdderStr (x,y,z))
by XBOOLE_1:79;
then A8:
( Following (s2,2) = (Following (t,2)) | the carrier of (GFA0CarryStr (x,y,z)) & Following (s2,3) = (Following (t,3)) | the carrier of (GFA0CarryStr (x,y,z)) )
by A3, FACIRC_1:31;
A9:
the carrier of (BitGFA0Str (x,y,z)) = the carrier of (GFA0AdderStr (x,y,z)) \/ the carrier of (GFA0CarryStr (x,y,z))
by CIRCCOMB:def 2;
A10:
( dom (Following (s1,2)) = the carrier of (GFA0AdderStr (x,y,z)) & dom (Following (s2,2)) = the carrier of (GFA0CarryStr (x,y,z)) )
by CIRCUIT1:3;
A11:
now for a being object st a in the carrier of (BitGFA0Str (x,y,z)) holds
(Following (s,2)) . a = (Following (Following (s,2))) . alet a be
object ;
( a in the carrier of (BitGFA0Str (x,y,z)) implies (Following (s,2)) . a = (Following (Following (s,2))) . a )assume
a in the
carrier of
(BitGFA0Str (x,y,z))
;
(Following (s,2)) . a = (Following (Following (s,2))) . athen
(
a in the
carrier of
(GFA0AdderStr (x,y,z)) or
a in the
carrier of
(GFA0CarryStr (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 (BitGFA0Str (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