set S = 1GateCircStr <*F₁()*>,F₆();
let s be State of (F₅() +* (1GateCircuit <*F₁()*>,F₆())); :: thesis: for s9 being State of F₅() st s9 = s | the carrier of F₄() holds
for a1 being Element of F₂() st ( F₁() in InnerVertices F₄() implies a1 = (Result s9) . F₁() ) & ( not F₁() in InnerVertices F₄() implies a1 = s . F₁() ) holds
(Result s) . (Output (1GateCircStr <*F₁()*>,F₆())) = F₃(a1)
let s9 be State of F₅(); :: thesis: ( s9 = s | the carrier of F₄() implies for a1 being Element of F₂() st ( F₁() in InnerVertices F₄() implies a1 = (Result s9) . F₁() ) & ( not F₁() in InnerVertices F₄() implies a1 = s . F₁() ) holds
(Result s) . (Output (1GateCircStr <*F₁()*>,F₆())) = F₃(a1) )
assume A3: s9 = s | the carrier of F₄() ; :: thesis: for a1 being Element of F₂() st ( F₁() in InnerVertices F₄() implies a1 = (Result s9) . F₁() ) & ( not F₁() in InnerVertices F₄() implies a1 = s . F₁() ) holds
(Result s) . (Output (1GateCircStr <*F₁()*>,F₆())) = F₃(a1)
rng <*F₁()*> = {F₁()} by FINSEQ_1:55;
then A4: ( InputVertices (1GateCircStr <*F₁()*>,F₆()) = rng <*F₁()*> & F₁() in rng <*F₁()*> ) by CIRCCOMB:49, TARSKI:def 1;
then A5: ( F₁() in InnerVertices F₄() or F₁() in (InputVertices (1GateCircStr <*F₁()*>,F₆())) \ (InnerVertices F₄()) ) by XBOOLE_0:def 5;
A6: s9 is stabilizing by Def2;
InnerVertices (1GateCircStr <*F₁()*>,F₆()) = {(Output (1GateCircStr <*F₁()*>,F₆()))} by Th17;
then A7: InputVertices F₄() misses InnerVertices (1GateCircStr <*F₁()*>,F₆()) by A2, ZFMISC_1:56;
then A8: (Following s,(stabilization-time s9)) | the carrier of F₄() = Following s9,(stabilization-time s9) by A3, Th30, CIRCCMB2:14
.= Result s9 by A6, Th2 ;
F₄() tolerates 1GateCircStr <*F₁()*>,F₆() by CIRCCOMB:55;
then InputVertices (F₄() +* (1GateCircStr <*F₁()*>,F₆())) = (InputVertices F₄()) \/ ((InputVertices (1GateCircStr <*F₁()*>,F₆())) \ (InnerVertices F₄())) by A7, FACIRC_1:4;
then A9: ( F₁() in InnerVertices F₄() or F₁() in InputVertices (F₄() +* (1GateCircStr <*F₁()*>,F₆())) ) by A5, XBOOLE_0:def 3;
let a1 be Element of F₂(); :: thesis: ( ( F₁() in InnerVertices F₄() implies a1 = (Result s9) . F₁() ) & ( not F₁() in InnerVertices F₄() implies a1 = s . F₁() ) implies (Result s) . (Output (1GateCircStr <*F₁()*>,F₆())) = F₃(a1) )
assume ( ( F₁() in InnerVertices F₄() implies a1 = (Result s9) . F₁() ) & ( not F₁() in InnerVertices F₄() implies a1 = s . F₁() ) ) ; :: thesis: (Result s) . (Output (1GateCircStr <*F₁()*>,F₆())) = F₃(a1)
then A10: a1 = (Following s,(stabilization-time s9)) . F₁() by A9, A8, Th1, FUNCT_1:72;
A11: s is stabilizing by Def2;
the carrier' of (1GateCircStr <*F₁()*>,F₆()) = {[<*F₁()*>,F₆()]} by CIRCCOMB:def 6;
then ( [<*F₁()*>,F₆()] in {[<*F₁()*>,F₆()]} & the carrier' of (F₄() +* (1GateCircStr <*F₁()*>,F₆())) = the carrier' of F₄() \/ {[<*F₁()*>,F₆()]} ) by CIRCCOMB:def 2, TARSKI:def 1;
then reconsider g = [<*F₁()*>,F₆()] as Gate of (F₄() +* (1GateCircStr <*F₁()*>,F₆())) by XBOOLE_0:def 3;
A12: the_result_sort_of g = the ResultSort of (F₄() +* (1GateCircStr <*F₁()*>,F₆())) . g by MSUALG_1:def 7
.= g by CIRCCOMB:52 ;
A13: g `2 = F<sub>6</sub>() by MCART_1:7;
the carrier of (F<sub>4</sub>() +* (1GateCircStr <*F<sub>1</sub>()*>,F<sub>6</sub>())) = the carrier of F<sub>4</sub>() \/ the carrier of (1GateCircStr <*F<sub>1</sub>()*>,F<sub>6</sub>()) by CIRCCOMB:def 2;
then A14: F<sub>1</sub>() in the carrier of (F<sub>4</sub>() +* (1GateCircStr <*F<sub>1</sub>()*>,F<sub>6</sub>())) by A4, XBOOLE_0:def 3;
A15: [<*F<sub>1</sub>()*>,F<sub>6</sub>()] = Output (1GateCircStr <*F<sub>1</sub>()*>,F<sub>6</sub>()) by Th16;
g = [(the Arity of (F<sub>4</sub>() +* (1GateCircStr <*F<sub>1</sub>()*>,F<sub>6</sub>())) . g),(g `2 )] by CIRCCOMB:def 8;
then A16: <*F₁()*> = the Arity of (F₄() +* (1GateCircStr <*F₁()*>,F₆())) . g by ZFMISC_1:33
.= the_arity_of g by MSUALG_1:def 6 ;
dom (Following s,(stabilization-time s9)) = the carrier of (F₄() +* (1GateCircStr <*F₁()*>,F₆())) by CIRCUIT1:4;
then A17: (Following s,(stabilization-time s9)) * <*F₁()*> = <*a1*> by A14, A10, FINSEQ_2:38;
stabilization-time s <= 1 + (stabilization-time s9) by A2, A3, Th52;
hence (Result s) . (Output (1GateCircStr <*F₁()*>,F₆())) = (Following s,(1 + (stabilization-time s9))) . (Output (1GateCircStr <*F₁()*>,F₆())) by A11, Th5
.= (Following (Following s,(stabilization-time s9))) . g by A15, FACIRC_1:12
.= F₆() . ((Following s,(stabilization-time s9)) * <*F₁()*>) by A12, A16, A13, FACIRC_1:34
.= F₃(a1) by A1, A17 ;
:: thesis: verum
F₅() tolerates 1GateCircuit <*F₁()*>,F₆() by Th30;
then the Sorts of F₅() tolerates the Sorts of (1GateCircuit <*F₁()*>,F₆()) by CIRCCOMB:def 3;
then reconsider s1 = (Following s,(stabilization-time s9)) | the carrier of (1GateCircStr <*F₁()*>,F₆()) as State of (1GateCircuit <*F₁()*>,F₆()) by CIRCCOMB:33;