set S = 1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉());
let s be State of (F₈() +* (1GateCircuit (<*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 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₄() ) holds
(Result s) . (Output (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉()))) = F₆(a1,a2,a3,a4)
let s9 be State of F₈(); :: thesis: ( s9 = s | the carrier of F₇() implies for a1, a2, a3, a4 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₄() ) holds
(Result s) . (Output (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉()))) = F₆(a1,a2,a3,a4) )
assume A3: s9 = s | the carrier of F₇() ; :: thesis: for a1, a2, a3, a4 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₄() ) holds
(Result s) . (Output (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉()))) = F₆(a1,a2,a3,a4)
A4: s9 is stabilizing by Def2;
InnerVertices (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉())) = {(Output (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉())))} by Th16;
then A5: InputVertices F₇() misses InnerVertices (1GateCircStr (<*F₁(),F₂(),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 ;
F₇() tolerates 1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉()) by CIRCCOMB:47;
then A7: InputVertices (F₇() +* (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉()))) = (InputVertices F₇()) \/ ((InputVertices (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉()))) \ (InnerVertices F₇())) by A5, FACIRC_1:4;
A8: [<*F₁(),F₂(),F₃(),F₄()*>,F₉()] = Output (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉())) by Th15;
A9: s is stabilizing by Def2;
A10: 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;
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;
let a1, a2, a3, a4 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₄() ) implies (Result s) . (Output (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉()))) = F₆(a1,a2,a3,a4) )
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₄() ) ) ; :: thesis: (Result s) . (Output (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉()))) = F₆(a1,a2,a3,a4)
A15: InputVertices (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉())) = rng <*F₁(),F₂(),F₃(),F₄()*> by CIRCCOMB:42;
A16: rng <*F₁(),F₂(),F₃(),F₄()*> = {F₁(),F₂(),F₃(),F₄()} by Th13;
then A17: F₃() in rng <*F₁(),F₂(),F₃(),F₄()*> by ENUMSET1:def 2;
then A18: F₃() in the carrier of (F₇() +* (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉()))) by A15, A10, XBOOLE_0:def 3;
A19: F₄() in rng <*F₁(),F₂(),F₃(),F₄()*> by A16, ENUMSET1:def 2;
then A20: F₄() in the carrier of (F₇() +* (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉()))) by A15, A10, XBOOLE_0:def 3;
A21: F₁() in rng <*F₁(),F₂(),F₃(),F₄()*> by A16, ENUMSET1:def 2;
then A22: F₁() in the carrier of (F₇() +* (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉()))) by A15, A10, XBOOLE_0:def 3;
( F₃() in InnerVertices F₇() or F₃() in (InputVertices (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉()))) \ (InnerVertices F₇()) ) by A15, A17, XBOOLE_0:def 5;
then ( F₃() in InnerVertices F₇() or F₃() in InputVertices (F₇() +* (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉()))) ) by A7, XBOOLE_0:def 3;
then A23: a3 = (Following (s,(stabilization-time s9))) . F₃() by A13, A6, Th1, FUNCT_1:49;
g = [( the Arity of (F₇() +* (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉()))) . g),(g `2)] by CIRCCOMB:def 8;
then A24: <*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 XTUPLE_0:1
.= the_arity_of g by MSUALG_1:def 1 ;
A25: g `2 = F₉() ;
( F₁() in InnerVertices F₇() or F₁() in (InputVertices (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉()))) \ (InnerVertices F₇()) ) by A15, A21, XBOOLE_0:def 5;
then ( F₁() in InnerVertices F₇() or F₁() in InputVertices (F₇() +* (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉()))) ) by A7, XBOOLE_0:def 3;
then A26: a1 = (Following (s,(stabilization-time s9))) . F₁() by A11, A6, Th1, FUNCT_1:49;
A27: F₂() in rng <*F₁(),F₂(),F₃(),F₄()*> by A16, ENUMSET1:def 2;
then A28: F₂() in the carrier of (F₇() +* (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉()))) by A15, A10, XBOOLE_0:def 3;
( F₄() in InnerVertices F₇() or F₄() in (InputVertices (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉()))) \ (InnerVertices F₇()) ) by A15, A19, XBOOLE_0:def 5;
then ( F₄() in InnerVertices F₇() or F₄() in InputVertices (F₇() +* (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉()))) ) by A7, XBOOLE_0:def 3;
then A29: a4 = (Following (s,(stabilization-time s9))) . F₄() by A14, A6, Th1, FUNCT_1:49;
( F₂() in InnerVertices F₇() or F₂() in (InputVertices (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉()))) \ (InnerVertices F₇()) ) by A15, A27, XBOOLE_0:def 5;
then ( F₂() in InnerVertices F₇() or F₂() in InputVertices (F₇() +* (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉()))) ) by A7, XBOOLE_0:def 3;
then A30: a2 = (Following (s,(stabilization-time s9))) . F₂() by A12, A6, Th1, FUNCT_1:49;
dom (Following (s,(stabilization-time s9))) = the carrier of (F₇() +* (1GateCircStr (<*F₁(),F₂(),F₃(),F₄()*>,F₉()))) by CIRCUIT1:3;
then A31: (Following (s,(stabilization-time s9))) * <*F₁(),F₂(),F₃(),F₄()*> = <*a1,a2,a3,a4*> by A22, A28, A18, A20, A26, A30, A23, A29, Th33;
A32: the_result_sort_of g = the ResultSort of (F₇() +* (1GateCircStr (<*F₁(),F₂(),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₃(),F₄()*>,F₉()))) = (Following (s,(1 + (stabilization-time s9)))) . (Output (1GateCircStr (<*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₄()*>) by A32, A24, A25, FACIRC_1:34
.= F₆(a1,a2,a3,a4) by A1, A31 ;
:: thesis: verum