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