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