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