set S = 1GateCircStr (<*F₁(),F₂()*>,F₇());
let s be State of (F₆() +* (1GateCircuit (<*F₁(),F₂()*>,F₇()))); :: thesis: for s9 being State of F₆() st s9 = s | the carrier of F₅() holds
for a1, a2 being Element of F₃() st ( F₁() in InnerVertices F₅() implies a1 = (Result s9) . F₁() ) & ( not F₁() in InnerVertices F₅() implies a1 = s . F₁() ) & ( F₂() in InnerVertices F₅() implies a2 = (Result s9) . F₂() ) & ( not F₂() in InnerVertices F₅() implies a2 = s . F₂() ) holds
(Result s) . (Output (1GateCircStr (<*F₁(),F₂()*>,F₇()))) = F₄(a1,a2)
let s9 be State of F₆(); :: thesis: ( s9 = s | the carrier of F₅() implies for a1, a2 being Element of F₃() st ( F₁() in InnerVertices F₅() implies a1 = (Result s9) . F₁() ) & ( not F₁() in InnerVertices F₅() implies a1 = s . F₁() ) & ( F₂() in InnerVertices F₅() implies a2 = (Result s9) . F₂() ) & ( not F₂() in InnerVertices F₅() implies a2 = s . F₂() ) holds
(Result s) . (Output (1GateCircStr (<*F₁(),F₂()*>,F₇()))) = F₄(a1,a2) )
assume A3: s9 = s | the carrier of F₅() ; :: thesis: for a1, a2 being Element of F₃() st ( F₁() in InnerVertices F₅() implies a1 = (Result s9) . F₁() ) & ( not F₁() in InnerVertices F₅() implies a1 = s . F₁() ) & ( F₂() in InnerVertices F₅() implies a2 = (Result s9) . F₂() ) & ( not F₂() in InnerVertices F₅() implies a2 = s . F₂() ) holds
(Result s) . (Output (1GateCircStr (<*F₁(),F₂()*>,F₇()))) = F₄(a1,a2)
A4: s9 is stabilizing by Def2;
InnerVertices (1GateCircStr (<*F₁(),F₂()*>,F₇())) = {(Output (1GateCircStr (<*F₁(),F₂()*>,F₇())))} by Th16;
then A5: InputVertices F₅() misses InnerVertices (1GateCircStr (<*F₁(),F₂()*>,F₇())) by A2, ZFMISC_1:50;
then A6: (Following (s,(stabilization-time s9))) | the carrier of F₅() = Following (s9,(stabilization-time s9)) by A3, Th27, CIRCCMB2:13
.= Result s9 by A4, Th2 ;
the carrier' of (1GateCircStr (<*F₁(),F₂()*>,F₇())) = {[<*F₁(),F₂()*>,F₇()]} by CIRCCOMB:def 6;
then ( [<*F₁(),F₂()*>,F₇()] in {[<*F₁(),F₂()*>,F₇()]} & the carrier' of (F₅() +* (1GateCircStr (<*F₁(),F₂()*>,F₇()))) = the carrier' of F₅() \/ {[<*F₁(),F₂()*>,F₇()]} ) by CIRCCOMB:def 2, TARSKI:def 1;
then reconsider g = [<*F₁(),F₂()*>,F₇()] as Gate of (F₅() +* (1GateCircStr (<*F₁(),F₂()*>,F₇()))) by XBOOLE_0:def 3;
let a1, a2 be Element of F₃(); :: thesis: ( ( F₁() in InnerVertices F₅() implies a1 = (Result s9) . F₁() ) & ( not F₁() in InnerVertices F₅() implies a1 = s . F₁() ) & ( F₂() in InnerVertices F₅() implies a2 = (Result s9) . F₂() ) & ( not F₂() in InnerVertices F₅() implies a2 = s . F₂() ) implies (Result s) . (Output (1GateCircStr (<*F₁(),F₂()*>,F₇()))) = F₄(a1,a2) )
assume that
A7: ( ( F₁() in InnerVertices F₅() implies a1 = (Result s9) . F₁() ) & ( not F₁() in InnerVertices F₅() implies a1 = s . F₁() ) ) and
A8: ( ( F₂() in InnerVertices F₅() implies a2 = (Result s9) . F₂() ) & ( not F₂() in InnerVertices F₅() implies a2 = s . F₂() ) ) ; :: thesis: (Result s) . (Output (1GateCircStr (<*F₁(),F₂()*>,F₇()))) = F₄(a1,a2)
A9: InputVertices (1GateCircStr (<*F₁(),F₂()*>,F₇())) = rng <*F₁(),F₂()*> by CIRCCOMB:42;
F₅() tolerates 1GateCircStr (<*F₁(),F₂()*>,F₇()) by CIRCCOMB:47;
then A10: InputVertices (F₅() +* (1GateCircStr (<*F₁(),F₂()*>,F₇()))) = (InputVertices F₅()) \/ ((InputVertices (1GateCircStr (<*F₁(),F₂()*>,F₇()))) \ (InnerVertices F₅())) by A5, FACIRC_1:4;
A11: rng <*F₁(),F₂()*> = {F₁(),F₂()} by FINSEQ_2:127;
then A12: F₂() in rng <*F₁(),F₂()*> by TARSKI:def 2;
then ( F₂() in InnerVertices F₅() or F₂() in (InputVertices (1GateCircStr (<*F₁(),F₂()*>,F₇()))) \ (InnerVertices F₅()) ) by A9, XBOOLE_0:def 5;
then ( F₂() in InnerVertices F₅() or F₂() in InputVertices (F₅() +* (1GateCircStr (<*F₁(),F₂()*>,F₇()))) ) by A10, XBOOLE_0:def 3;
then A13: a2 = (Following (s,(stabilization-time s9))) . F₂() by A8, A6, Th1, FUNCT_1:49;
A14: F₁() in rng <*F₁(),F₂()*> by A11, TARSKI:def 2;
then ( F₁() in InnerVertices F₅() or F₁() in (InputVertices (1GateCircStr (<*F₁(),F₂()*>,F₇()))) \ (InnerVertices F₅()) ) by A9, XBOOLE_0:def 5;
then ( F₁() in InnerVertices F₅() or F₁() in InputVertices (F₅() +* (1GateCircStr (<*F₁(),F₂()*>,F₇()))) ) by A10, XBOOLE_0:def 3;
then A15: a1 = (Following (s,(stabilization-time s9))) . F₁() by A7, A6, Th1, FUNCT_1:49;
g = [( the Arity of (F₅() +* (1GateCircStr (<*F₁(),F₂()*>,F₇()))) . g),(g `2)] by CIRCCOMB:def 8;
then A16: <*F<sub>1</sub>(),F<sub>2</sub>()*> = the Arity of (F<sub>5</sub>() +* (1GateCircStr (<*F<sub>1</sub>(),F<sub>2</sub>()*>,F<sub>7</sub>()))) . g by XTUPLE_0:1
.= the_arity_of g by MSUALG_1:def 1 ;
A17: g `2 = F₇() ;
A18: the carrier of (F₅() +* (1GateCircStr (<*F₁(),F₂()*>,F₇()))) = the carrier of F₅() \/ the carrier of (1GateCircStr (<*F₁(),F₂()*>,F₇())) by CIRCCOMB:def 2;
then A19: F₂() in the carrier of (F₅() +* (1GateCircStr (<*F₁(),F₂()*>,F₇()))) by A9, A12, XBOOLE_0:def 3;
A20: [<*F₁(),F₂()*>,F₇()] = Output (1GateCircStr (<*F₁(),F₂()*>,F₇())) by Th15;
A21: s is stabilizing by Def2;
A22: dom (Following (s,(stabilization-time s9))) = the carrier of (F₅() +* (1GateCircStr (<*F₁(),F₂()*>,F₇()))) by CIRCUIT1:3;
F₁() in the carrier of (F₅() +* (1GateCircStr (<*F₁(),F₂()*>,F₇()))) by A9, A14, A18, XBOOLE_0:def 3;
then A23: (Following (s,(stabilization-time s9))) * <*F₁(),F₂()*> = <*a1,a2*> by A19, A15, A13, A22, FINSEQ_2:125;
A24: the_result_sort_of g = the ResultSort of (F₅() +* (1GateCircStr (<*F₁(),F₂()*>,F₇()))) . g by MSUALG_1:def 2
.= g by CIRCCOMB:44 ;
stabilization-time s <= 1 + (stabilization-time s9) by A2, A3, Th48;
hence (Result s) . (Output (1GateCircStr (<*F₁(),F₂()*>,F₇()))) = (Following (s,(1 + (stabilization-time s9)))) . (Output (1GateCircStr (<*F₁(),F₂()*>,F₇()))) by A21, Th5
.= (Following (Following (s,(stabilization-time s9)))) . g by A20, FACIRC_1:12
.= F₇() . ((Following (s,(stabilization-time s9))) * <*F₁(),F₂()*>) by A24, A16, A17, FACIRC_1:34
.= F₄(a1,a2) by A1, A23 ;
:: thesis: verum