let n be Nat; for ap, bm, cp, dm being nonpair-yielding FinSeqLen of n
for s being State of (n -BitFTA1Circ (ap,bm,cp,dm)) holds Following (s,4) is stable
let ap, bm, cp, dm be nonpair-yielding FinSeqLen of n; for s being State of (n -BitFTA1Circ (ap,bm,cp,dm)) holds Following (s,4) is stable
let s be State of (n -BitFTA1Circ (ap,bm,cp,dm)); Following (s,4) is stable
set S1 = n -BitFTA1Layer1Str (ap,bm,cp);
set S2 = n -BitFTA1Layer2Str (ap,bm,cp,dm);
set C1 = n -BitFTA1Layer1Circ (ap,bm,cp);
set C2 = n -BitFTA1Layer2Circ (ap,bm,cp,dm);
set S = n -BitFTA1Str (ap,bm,cp,dm);
set C = n -BitFTA1Circ (ap,bm,cp,dm);
A1:
n -BitFTA1Str (ap,bm,cp,dm) = (n -BitFTA1Layer1Str (ap,bm,cp)) +* (n -BitFTA1Layer2Str (ap,bm,cp,dm))
by Th16;
A2:
n -BitFTA1Circ (ap,bm,cp,dm) = (n -BitFTA1Layer1Circ (ap,bm,cp)) +* (n -BitFTA1Layer2Circ (ap,bm,cp,dm))
by Th17;
A3:
n -BitFTA1Layer1Circ (ap,bm,cp) tolerates n -BitFTA1Layer2Circ (ap,bm,cp,dm)
by CIRCCOMB:60;
A4:
the Sorts of (n -BitFTA1Layer1Circ (ap,bm,cp)) tolerates the Sorts of (n -BitFTA1Layer2Circ (ap,bm,cp,dm))
by A3, CIRCCOMB:def 3;
reconsider t = s as State of ((n -BitFTA1Layer1Circ (ap,bm,cp)) +* (n -BitFTA1Layer2Circ (ap,bm,cp,dm))) by A2;
reconsider s1 = t | the carrier of (n -BitFTA1Layer1Str (ap,bm,cp)) as State of (n -BitFTA1Layer1Circ (ap,bm,cp)) by A4, CIRCCOMB:26;
reconsider s2 = (Following (t,2)) | the carrier of (n -BitFTA1Layer2Str (ap,bm,cp,dm)) as State of (n -BitFTA1Layer2Circ (ap,bm,cp,dm)) by A4, CIRCCOMB:26;
A5:
InputVertices (n -BitFTA1Layer1Str (ap,bm,cp)) misses InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm))
by Th18;
A6:
Following (s1,2) is stable
by Th19;
A7:
Following (s2,2) is stable
proof
set c0 =
[<*>,((0 -tuples_on BOOLEAN) --> FALSE)];
B1:
[<*>,((0 -tuples_on BOOLEAN) --> FALSE)] in InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm))
by LmT1Cin0In;
B2:
n -BitFTA1Layer1Str (
ap,
bm,
cp)
tolerates n -BitFTA1Layer2Str (
ap,
bm,
cp,
dm)
by CIRCCOMB:47;
InnerVertices (n -BitFTA1Str (ap,bm,cp,dm)) = (InnerVertices (n -BitFTA1Layer1Str (ap,bm,cp))) \/ (InnerVertices (n -BitFTA1Layer2Str (ap,bm,cp,dm)))
by A1, B2, CIRCCOMB:11;
then B3:
[<*>,((0 -tuples_on BOOLEAN) --> FALSE)] in InnerVertices (n -BitFTA1Str (ap,bm,cp,dm))
by B1, XBOOLE_0:def 3;
reconsider Cb =
n -BitFTA1Circ (
ap,
bm,
cp,
dm) as
non-empty gate`2=den Boolean Circuit of
n -BitFTA1Str (
ap,
bm,
cp,
dm) ;
reconsider s9 =
s as
State of
Cb ;
B5:
(Following (Following s9)) . [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] = FALSE
by B3, Th9;
s2 . [<*>,((0 -tuples_on BOOLEAN) --> FALSE)] =
(Following (t,2)) . [<*>,((0 -tuples_on BOOLEAN) --> FALSE)]
by FUNCT_1:49, B1
.=
FALSE
by A1, A2, FACIRC_1:15, B5
;
hence
Following (
s2,2) is
stable
by Th20;
verum
end;
Following (t,(2 + 2)) is stable
by CIRCCOMB:60, A5, A6, A7, CIRCCMB2:19;
hence
Following (s,4) is stable
by A1, A2; verum