set S = 1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀();
let s be State of (F₉() +* (1GateCircuit <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())); :: thesis: for s9 being State of F₉() st s9 = s | the carrier of F₈() holds
for a1, a2, a3, a4, a5 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₂() ) & ( F₃() in InnerVertices F₈() implies a3 = (Result s9) . F₃() ) & ( not F₃() in InnerVertices F₈() implies a3 = s . F₃() ) & ( F₄() in InnerVertices F₈() implies a4 = (Result s9) . F₄() ) & ( not F₄() in InnerVertices F₈() implies a4 = s . F₄() ) & ( F₅() in InnerVertices F₈() implies a5 = (Result s9) . F₅() ) & ( not F₅() in InnerVertices F₈() implies a5 = s . F₅() ) holds
(Result s) . (Output (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) = F₇(a1,a2,a3,a4,a5)
let s9 be State of F₉(); :: thesis: ( s9 = s | the carrier of F₈() implies for a1, a2, a3, a4, a5 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₂() ) & ( F₃() in InnerVertices F₈() implies a3 = (Result s9) . F₃() ) & ( not F₃() in InnerVertices F₈() implies a3 = s . F₃() ) & ( F₄() in InnerVertices F₈() implies a4 = (Result s9) . F₄() ) & ( not F₄() in InnerVertices F₈() implies a4 = s . F₄() ) & ( F₅() in InnerVertices F₈() implies a5 = (Result s9) . F₅() ) & ( not F₅() in InnerVertices F₈() implies a5 = s . F₅() ) holds
(Result s) . (Output (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) = F₇(a1,a2,a3,a4,a5) )
assume A3: s9 = s | the carrier of F₈() ; :: thesis: for a1, a2, a3, a4, a5 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₂() ) & ( F₃() in InnerVertices F₈() implies a3 = (Result s9) . F₃() ) & ( not F₃() in InnerVertices F₈() implies a3 = s . F₃() ) & ( F₄() in InnerVertices F₈() implies a4 = (Result s9) . F₄() ) & ( not F₄() in InnerVertices F₈() implies a4 = s . F₄() ) & ( F₅() in InnerVertices F₈() implies a5 = (Result s9) . F₅() ) & ( not F₅() in InnerVertices F₈() implies a5 = s . F₅() ) holds
(Result s) . (Output (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) = F₇(a1,a2,a3,a4,a5)
A4: s9 is stabilizing by Def2;
InnerVertices (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀()) = {(Output (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀()))} by Th17;
then A5: InputVertices F₈() misses InnerVertices (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀()) by A2, ZFMISC_1:56;
then A6: (Following s,(stabilization-time s9)) | the carrier of F₈() = Following s9,(stabilization-time s9) by A3, Th30, CIRCCMB2:14
.= Result s9 by A4, Th2 ;
F₈() tolerates 1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀() by CIRCCOMB:55;
then A7: InputVertices (F₈() +* (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) = (InputVertices F₈()) \/ ((InputVertices (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) \ (InnerVertices F₈())) by A5, FACIRC_1:4;
A8: [<*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀()] = Output (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀()) by Th16;
A9: s is stabilizing by Def2;
A10: the carrier of (F₈() +* (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) = the carrier of F₈() \/ the carrier of (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀()) by CIRCCOMB:def 2;
the carrier' of (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀()) = {[<*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀()]} by CIRCCOMB:def 6;
then ( [<*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀()] in {[<*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀()]} & the carrier' of (F₈() +* (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) = the carrier' of F₈() \/ {[<*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀()]} ) by CIRCCOMB:def 2, TARSKI:def 1;
then reconsider g = [<*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀()] as Gate of (F₈() +* (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) by XBOOLE_0:def 3;
let a1, a2, a3, a4, a5 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₂() ) & ( F₃() in InnerVertices F₈() implies a3 = (Result s9) . F₃() ) & ( not F₃() in InnerVertices F₈() implies a3 = s . F₃() ) & ( F₄() in InnerVertices F₈() implies a4 = (Result s9) . F₄() ) & ( not F₄() in InnerVertices F₈() implies a4 = s . F₄() ) & ( F₅() in InnerVertices F₈() implies a5 = (Result s9) . F₅() ) & ( not F₅() in InnerVertices F₈() implies a5 = s . F₅() ) implies (Result s) . (Output (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) = F₇(a1,a2,a3,a4,a5) )
assume that
A11: ( ( F₁() in InnerVertices F₈() implies a1 = (Result s9) . F₁() ) & ( not F₁() in InnerVertices F₈() implies a1 = s . F₁() ) ) and
A12: ( ( F₂() in InnerVertices F₈() implies a2 = (Result s9) . F₂() ) & ( not F₂() in InnerVertices F₈() implies a2 = s . F₂() ) ) and
A13: ( ( F₃() in InnerVertices F₈() implies a3 = (Result s9) . F₃() ) & ( not F₃() in InnerVertices F₈() implies a3 = s . F₃() ) ) and
A14: ( ( F₄() in InnerVertices F₈() implies a4 = (Result s9) . F₄() ) & ( not F₄() in InnerVertices F₈() implies a4 = s . F₄() ) ) and
A15: ( ( F₅() in InnerVertices F₈() implies a5 = (Result s9) . F₅() ) & ( not F₅() in InnerVertices F₈() implies a5 = s . F₅() ) ) ; :: thesis: (Result s) . (Output (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) = F₇(a1,a2,a3,a4,a5)
A16: InputVertices (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀()) = rng <*F₁(),F₂(),F₃(),F₄(),F₅()*> by CIRCCOMB:49;
A17: rng <*F₁(),F₂(),F₃(),F₄(),F₅()*> = {F₁(),F₂(),F₃(),F₄(),F₅()} by Th15;
then A18: F₁() in rng <*F₁(),F₂(),F₃(),F₄(),F₅()*> by ENUMSET1:def 3;
then A19: F₁() in the carrier of (F₈() +* (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) by A16, A10, XBOOLE_0:def 3;
A20: F₅() in rng <*F₁(),F₂(),F₃(),F₄(),F₅()*> by A17, ENUMSET1:def 3;
then A21: F₅() in the carrier of (F₈() +* (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) by A16, A10, XBOOLE_0:def 3;
( F₅() in InnerVertices F₈() or F₅() in (InputVertices (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) \ (InnerVertices F₈()) ) by A16, A20, XBOOLE_0:def 5;
then ( F₅() in InnerVertices F₈() or F₅() in InputVertices (F₈() +* (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) ) by A7, XBOOLE_0:def 3;
then A22: a5 = (Following s,(stabilization-time s9)) . F₅() by A15, A6, Th1, FUNCT_1:72;
A23: F₄() in rng <*F₁(),F₂(),F₃(),F₄(),F₅()*> by A17, ENUMSET1:def 3;
then A24: F₄() in the carrier of (F₈() +* (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) by A16, A10, XBOOLE_0:def 3;
A25: F₃() in rng <*F₁(),F₂(),F₃(),F₄(),F₅()*> by A17, ENUMSET1:def 3;
then A26: F₃() in the carrier of (F₈() +* (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) by A16, A10, XBOOLE_0:def 3;
( F₃() in InnerVertices F₈() or F₃() in (InputVertices (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) \ (InnerVertices F₈()) ) by A16, A25, XBOOLE_0:def 5;
then ( F₃() in InnerVertices F₈() or F₃() in InputVertices (F₈() +* (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) ) by A7, XBOOLE_0:def 3;
then A27: a3 = (Following s,(stabilization-time s9)) . F₃() by A13, A6, Th1, FUNCT_1:72;
A28: F₂() in rng <*F₁(),F₂(),F₃(),F₄(),F₅()*> by A17, ENUMSET1:def 3;
then A29: F₂() in the carrier of (F₈() +* (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) by A16, A10, XBOOLE_0:def 3;
( F₁() in InnerVertices F₈() or F₁() in (InputVertices (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) \ (InnerVertices F₈()) ) by A16, A18, XBOOLE_0:def 5;
then ( F₁() in InnerVertices F₈() or F₁() in InputVertices (F₈() +* (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) ) by A7, XBOOLE_0:def 3;
then A30: a1 = (Following s,(stabilization-time s9)) . F₁() by A11, A6, Th1, FUNCT_1:72;
g = [(the Arity of (F₈() +* (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) . g),(g `2 )] by CIRCCOMB:def 8;
then A31: <*F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>(),F<sub>5</sub>()*> = the Arity of (F<sub>8</sub>() +* (1GateCircStr <*F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>(),F<sub>5</sub>()*>,F<sub>10</sub>())) . g by ZFMISC_1:33
.= the_arity_of g by MSUALG_1:def 6 ;
A32: g `2 = F₁₀() by MCART_1:7;
( F₄() in InnerVertices F₈() or F₄() in (InputVertices (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) \ (InnerVertices F₈()) ) by A16, A23, XBOOLE_0:def 5;
then ( F₄() in InnerVertices F₈() or F₄() in InputVertices (F₈() +* (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) ) by A7, XBOOLE_0:def 3;
then A33: a4 = (Following s,(stabilization-time s9)) . F₄() by A14, A6, Th1, FUNCT_1:72;
( F₂() in InnerVertices F₈() or F₂() in (InputVertices (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) \ (InnerVertices F₈()) ) by A16, A28, XBOOLE_0:def 5;
then ( F₂() in InnerVertices F₈() or F₂() in InputVertices (F₈() +* (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) ) by A7, XBOOLE_0:def 3;
then A34: a2 = (Following s,(stabilization-time s9)) . F₂() by A12, A6, Th1, FUNCT_1:72;
dom (Following s,(stabilization-time s9)) = the carrier of (F₈() +* (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) by CIRCUIT1:4;
then A35: (Following s,(stabilization-time s9)) * <*F₁(),F₂(),F₃(),F₄(),F₅()*> = <*a1,a2,a3,a4,a5*> by A19, A29, A26, A24, A21, A30, A34, A27, A33, A22, Th38;
A36: the_result_sort_of g = the ResultSort of (F₈() +* (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) . g by MSUALG_1:def 7
.= g by CIRCCOMB:52 ;
stabilization-time s <= 1 + (stabilization-time s9) by A2, A3, Th52;
hence (Result s) . (Output (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) = (Following s,(1 + (stabilization-time s9))) . (Output (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀())) by A9, Th5
.= (Following (Following s,(stabilization-time s9))) . g by A8, FACIRC_1:12
.= F₁₀() . ((Following s,(stabilization-time s9)) * <*F₁(),F₂(),F₃(),F₄(),F₅()*>) by A36, A31, A32, FACIRC_1:34
.= F₇(a1,a2,a3,a4,a5) by A1, A35 ;
:: thesis: verum
F₉() tolerates 1GateCircuit <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀() by Th30;
then the Sorts of F₉() tolerates the Sorts of (1GateCircuit <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀()) by CIRCCOMB:def 3;
then reconsider s1 = (Following s,(stabilization-time s9)) | the carrier of (1GateCircStr <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀()) as State of (1GateCircuit <*F₁(),F₂(),F₃(),F₄(),F₅()*>,F₁₀()) by CIRCCOMB:33;