let n be Nat; for ap, bp, cp, dp being nonpair-yielding FinSeqLen of n
for s being State of (n -BitFTA0Circ (ap,bp,cp,dp)) holds Following (s,4) is stable
let ap, bp, cp, dp be nonpair-yielding FinSeqLen of n; for s being State of (n -BitFTA0Circ (ap,bp,cp,dp)) holds Following (s,4) is stable
let s be State of (n -BitFTA0Circ (ap,bp,cp,dp)); Following (s,4) is stable
set S1 = n -BitFTA0Layer1Str (ap,bp,cp);
set S2 = n -BitFTA0Layer2Str (ap,bp,cp,dp);
set C1 = n -BitFTA0Layer1Circ (ap,bp,cp);
set C2 = n -BitFTA0Layer2Circ (ap,bp,cp,dp);
set S = n -BitFTA0Str (ap,bp,cp,dp);
set C = n -BitFTA0Circ (ap,bp,cp,dp);
A1:
n -BitFTA0Str (ap,bp,cp,dp) = (n -BitFTA0Layer1Str (ap,bp,cp)) +* (n -BitFTA0Layer2Str (ap,bp,cp,dp))
by Th5;
A2:
n -BitFTA0Circ (ap,bp,cp,dp) = (n -BitFTA0Layer1Circ (ap,bp,cp)) +* (n -BitFTA0Layer2Circ (ap,bp,cp,dp))
by Th6;
A3:
n -BitFTA0Layer1Circ (ap,bp,cp) tolerates n -BitFTA0Layer2Circ (ap,bp,cp,dp)
by CIRCCOMB:60;
A4:
the Sorts of (n -BitFTA0Layer1Circ (ap,bp,cp)) tolerates the Sorts of (n -BitFTA0Layer2Circ (ap,bp,cp,dp))
by A3, CIRCCOMB:def 3;
reconsider t = s as State of ((n -BitFTA0Layer1Circ (ap,bp,cp)) +* (n -BitFTA0Layer2Circ (ap,bp,cp,dp))) by A2;
reconsider s1 = t | the carrier of (n -BitFTA0Layer1Str (ap,bp,cp)) as State of (n -BitFTA0Layer1Circ (ap,bp,cp)) by A4, CIRCCOMB:26;
reconsider s2 = (Following (t,2)) | the carrier of (n -BitFTA0Layer2Str (ap,bp,cp,dp)) as State of (n -BitFTA0Layer2Circ (ap,bp,cp,dp)) by A4, CIRCCOMB:26;
A5:
InputVertices (n -BitFTA0Layer1Str (ap,bp,cp)) misses InnerVertices (n -BitFTA0Layer2Str (ap,bp,cp,dp))
by Th7;
A6:
Following (s1,2) is stable
by Th8;
A7:
Following (s2,2) is stable
proof
set c0 =
[<*>,((0 -tuples_on BOOLEAN) --> FALSE)];
B1:
[<*>,((0 -tuples_on BOOLEAN) --> FALSE)] in InnerVertices (n -BitFTA0Layer2Str (ap,bp,cp,dp))
by LmT0Cin0In;
B2:
n -BitFTA0Layer1Str (
ap,
bp,
cp)
tolerates n -BitFTA0Layer2Str (
ap,
bp,
cp,
dp)
by CIRCCOMB:47;
InnerVertices (n -BitFTA0Str (ap,bp,cp,dp)) = (InnerVertices (n -BitFTA0Layer1Str (ap,bp,cp))) \/ (InnerVertices (n -BitFTA0Layer2Str (ap,bp,cp,dp)))
by A1, B2, CIRCCOMB:11;
then B3:
[<*>,((0 -tuples_on BOOLEAN) --> FALSE)] in InnerVertices (n -BitFTA0Str (ap,bp,cp,dp))
by B1, XBOOLE_0:def 3;
reconsider Cb =
n -BitFTA0Circ (
ap,
bp,
cp,
dp) as
non-empty gate`2=den Boolean Circuit of
n -BitFTA0Str (
ap,
bp,
cp,
dp) ;
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 Th10;
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