let n be Nat; :: thesis: for ap, bp, cp being nonpair-yielding FinSequence
for s being State of (n -BitFTA0Layer1Circ (ap,bp,cp)) holds Following (s,2) is stable
let ap, bp, cp be nonpair-yielding FinSequence; :: thesis: for s being State of (n -BitFTA0Layer1Circ (ap,bp,cp)) holds Following (s,2) is stable
set A0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE));
defpred S₁[ Nat] means for s being State of ($1 -BitFTA0Layer1Circ (ap,bp,cp)) holds Following (s,2) is stable ;
A1: 0 -BitFTA0Layer1Circ (ap,bp,cp) = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE))

proof

consider f, g being ManySortedSet of NAT such that
0 -BitFTA0Layer1Str (ap,bp,cp) = f . 0 and
B1: 0 -BitFTA0Layer1Circ (ap,bp,cp) = g . 0 and
f . 0 = 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and
B2: g . 0 = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) and
for k being Nat
for S being non empty ManySortedSign
for A being non-empty MSAlgebra over S st S = f . k & A = g . k holds
( f . (k + 1) = S +* (BitGFA0Str ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) & g . (k + 1) = A +* (BitGFA0Circ ((ap . (k + 1)),(bp . (k + 1)),(cp . (k + 1)))) ) by Def5;
thus 0 -BitFTA0Layer1Circ (ap,bp,cp) = 1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) by B1, B2; :: thesis: verum

end;

A2: S₁[ 0 ]

proof

let s be State of (0 -BitFTA0Layer1Circ (ap,bp,cp)); :: thesis: Following (s,2) is stable
reconsider s0 = s as State of (1GateCircuit (<*>,((0 -tuples_on BOOLEAN) --> FALSE))) by A1;
B1: Following (s0,1) = Following s0 by FACIRC_1:14;
B2: Following (s0,2) = Following (s0,1) by B1, CIRCCMB2:2, CIRCCMB2:4;
B3: 1GateCircStr (<*>,((0 -tuples_on BOOLEAN) --> FALSE)) = 0 -BitFTA0Layer1Str (ap,bp,cp) by LmT00L1;
thus Following (s,2) is stable by B3, A1, B2, B1, CIRCCMB2:2; :: thesis: verum

end;

A3: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume B1: S₁[i] ; :: thesis: S₁[i + 1]
reconsider S1 = i -BitFTA0Layer1Str (ap,bp,cp) as non empty non void Circuit-like ManySortedSign ;
set B = BitGFA0Str ((ap . (i + 1)),(bp . (i + 1)),(cp . (i + 1)));
reconsider B = BitGFA0Str ((ap . (i + 1)),(bp . (i + 1)),(cp . (i + 1))) as non empty non void Circuit-like ManySortedSign ;
reconsider SS = (i + 1) -BitFTA0Layer1Str (ap,bp,cp) as non empty non void Circuit-like ManySortedSign ;
reconsider A1a = i -BitFTA0Layer1Circ (ap,bp,cp) as non-empty Circuit of S1 ;
reconsider Ba = BitGFA0Circ ((ap . (i + 1)),(bp . (i + 1)),(cp . (i + 1))) as non-empty Circuit of B ;
reconsider AA = (i + 1) -BitFTA0Layer1Circ (ap,bp,cp) as non-empty Circuit of SS ;
B2: AA = A1a +* Ba by LmT06A;
B3: A1a tolerates Ba by CIRCCOMB:60;
InputVertices S1 is without_pairs by LmT0L1wp;
then B4: InputVertices S1 misses InnerVertices B by GFACIRC1:32, FACIRC_1:5;
InputVertices B is without_pairs by GFACIRC1:35;
then B5: InputVertices B misses InnerVertices S1 by LmT0L1rel, FACIRC_1:5;
B6: for s being State of Ba holds Following (s,2) is stable by GFACIRC1:40;

now :: thesis: for s being State of AA holds Following (s,2) is stable

let s be State of AA; :: thesis: Following (s,2) is stable
C1: Following (s,2) is stable

proof

2 = max (2,2) ;
hence Following (s,2) is stable by LmT05A, B2, B3, B4, B5, B1, B6, CIRCCMB2:24; :: thesis: verum

end;

thus Following (s,2) is stable by C1; :: thesis: verum

end;

hence S₁[i + 1] ; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A2, A3);
hence for s being State of (n -BitFTA0Layer1Circ (ap,bp,cp)) holds Following (s,2) is stable ; :: thesis: verum