set S = 1GateCircStr <*F1(),F2()*>,F7();
let s be State of (F6() +* (1GateCircuit <*F1(),F2()*>,F7())); :: thesis: for s9 being State of F6() st s9 = s | the carrier of F5() holds
for a1, a2 being Element of F3() st ( F1() in InnerVertices F5() implies a1 = (Result s9) . F1() ) & ( not F1() in InnerVertices F5() implies a1 = s . F1() ) & ( F2() in InnerVertices F5() implies a2 = (Result s9) . F2() ) & ( not F2() in InnerVertices F5() implies a2 = s . F2() ) holds
(Result s) . (Output (1GateCircStr <*F1(),F2()*>,F7())) = F4(a1,a2)
let s9 be State of F6(); :: thesis: ( s9 = s | the carrier of F5() implies for a1, a2 being Element of F3() st ( F1() in InnerVertices F5() implies a1 = (Result s9) . F1() ) & ( not F1() in InnerVertices F5() implies a1 = s . F1() ) & ( F2() in InnerVertices F5() implies a2 = (Result s9) . F2() ) & ( not F2() in InnerVertices F5() implies a2 = s . F2() ) holds
(Result s) . (Output (1GateCircStr <*F1(),F2()*>,F7())) = F4(a1,a2) )
assume A3: s9 = s | the carrier of F5() ; :: thesis: for a1, a2 being Element of F3() st ( F1() in InnerVertices F5() implies a1 = (Result s9) . F1() ) & ( not F1() in InnerVertices F5() implies a1 = s . F1() ) & ( F2() in InnerVertices F5() implies a2 = (Result s9) . F2() ) & ( not F2() in InnerVertices F5() implies a2 = s . F2() ) holds
(Result s) . (Output (1GateCircStr <*F1(),F2()*>,F7())) = F4(a1,a2)
A4: s9 is stabilizing by Def2;
InnerVertices (1GateCircStr <*F1(),F2()*>,F7()) = {(Output (1GateCircStr <*F1(),F2()*>,F7()))} by Th17;
then A5: InputVertices F5() misses InnerVertices (1GateCircStr <*F1(),F2()*>,F7()) by A2, ZFMISC_1:56;
then A6: (Following s,(stabilization-time s9)) | the carrier of F5() = Following s9,(stabilization-time s9) by A3, Th30, CIRCCMB2:14
.= Result s9 by A4, Th2 ;
the carrier' of (1GateCircStr <*F1(),F2()*>,F7()) = {[<*F1(),F2()*>,F7()]} by CIRCCOMB:def 6;
then ( [<*F1(),F2()*>,F7()] in {[<*F1(),F2()*>,F7()]} & the carrier' of (F5() +* (1GateCircStr <*F1(),F2()*>,F7())) = the carrier' of F5() \/ {[<*F1(),F2()*>,F7()]} ) by CIRCCOMB:def 2, TARSKI:def 1;
then reconsider g = [<*F1(),F2()*>,F7()] as Gate of (F5() +* (1GateCircStr <*F1(),F2()*>,F7())) by XBOOLE_0:def 3;
let a1, a2 be Element of F3(); :: thesis: ( ( F1() in InnerVertices F5() implies a1 = (Result s9) . F1() ) & ( not F1() in InnerVertices F5() implies a1 = s . F1() ) & ( F2() in InnerVertices F5() implies a2 = (Result s9) . F2() ) & ( not F2() in InnerVertices F5() implies a2 = s . F2() ) implies (Result s) . (Output (1GateCircStr <*F1(),F2()*>,F7())) = F4(a1,a2) )
assume that
A7: ( ( F1() in InnerVertices F5() implies a1 = (Result s9) . F1() ) & ( not F1() in InnerVertices F5() implies a1 = s . F1() ) ) and
A8: ( ( F2() in InnerVertices F5() implies a2 = (Result s9) . F2() ) & ( not F2() in InnerVertices F5() implies a2 = s . F2() ) ) ; :: thesis: (Result s) . (Output (1GateCircStr <*F1(),F2()*>,F7())) = F4(a1,a2)
A9: InputVertices (1GateCircStr <*F1(),F2()*>,F7()) = rng <*F1(),F2()*> by CIRCCOMB:49;
F5() tolerates 1GateCircStr <*F1(),F2()*>,F7() by CIRCCOMB:55;
then A10: InputVertices (F5() +* (1GateCircStr <*F1(),F2()*>,F7())) = (InputVertices F5()) \/ ((InputVertices (1GateCircStr <*F1(),F2()*>,F7())) \ (InnerVertices F5())) by A5, FACIRC_1:4;
A11: rng <*F1(),F2()*> = {F1(),F2()} by FINSEQ_2:147;
then A12: F2() in rng <*F1(),F2()*> by TARSKI:def 2;
then ( F2() in InnerVertices F5() or F2() in (InputVertices (1GateCircStr <*F1(),F2()*>,F7())) \ (InnerVertices F5()) ) by A9, XBOOLE_0:def 5;
then ( F2() in InnerVertices F5() or F2() in InputVertices (F5() +* (1GateCircStr <*F1(),F2()*>,F7())) ) by A10, XBOOLE_0:def 3;
then A13: a2 = (Following s,(stabilization-time s9)) . F2() by A8, A6, Th1, FUNCT_1:72;
A14: F1() in rng <*F1(),F2()*> by A11, TARSKI:def 2;
then ( F1() in InnerVertices F5() or F1() in (InputVertices (1GateCircStr <*F1(),F2()*>,F7())) \ (InnerVertices F5()) ) by A9, XBOOLE_0:def 5;
then ( F1() in InnerVertices F5() or F1() in InputVertices (F5() +* (1GateCircStr <*F1(),F2()*>,F7())) ) by A10, XBOOLE_0:def 3;
then A15: a1 = (Following s,(stabilization-time s9)) . F1() by A7, A6, Th1, FUNCT_1:72;
g = [(the Arity of (F5() +* (1GateCircStr <*F1(),F2()*>,F7())) . g),(g `2 )] by CIRCCOMB:def 8;
then A16: <*F1(),F2()*> = the Arity of (F5() +* (1GateCircStr <*F1(),F2()*>,F7())) . g by ZFMISC_1:33
.= the_arity_of g by MSUALG_1:def 6 ;
A17: g `2 = F7() by MCART_1:7;
A18: the carrier of (F5() +* (1GateCircStr <*F1(),F2()*>,F7())) = the carrier of F5() \/ the carrier of (1GateCircStr <*F1(),F2()*>,F7()) by CIRCCOMB:def 2;
then A19: F2() in the carrier of (F5() +* (1GateCircStr <*F1(),F2()*>,F7())) by A9, A12, XBOOLE_0:def 3;
A20: [<*F1(),F2()*>,F7()] = Output (1GateCircStr <*F1(),F2()*>,F7()) by Th16;
A21: s is stabilizing by Def2;
A22: dom (Following s,(stabilization-time s9)) = the carrier of (F5() +* (1GateCircStr <*F1(),F2()*>,F7())) by CIRCUIT1:4;
F1() in the carrier of (F5() +* (1GateCircStr <*F1(),F2()*>,F7())) by A9, A14, A18, XBOOLE_0:def 3;
then A23: (Following s,(stabilization-time s9)) * <*F1(),F2()*> = <*a1,a2*> by A19, A15, A13, A22, FINSEQ_2:145;
A24: the_result_sort_of g = the ResultSort of (F5() +* (1GateCircStr <*F1(),F2()*>,F7())) . 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 <*F1(),F2()*>,F7())) = (Following s,(1 + (stabilization-time s9))) . (Output (1GateCircStr <*F1(),F2()*>,F7())) by A21, Th5
.= (Following (Following s,(stabilization-time s9))) . g by A20, FACIRC_1:12
.= F7() . ((Following s,(stabilization-time s9)) * <*F1(),F2()*>) by A24, A16, A17, FACIRC_1:34
.= F4(a1,a2) by A1, A23 ;
:: thesis: verum
F6() tolerates 1GateCircuit <*F1(),F2()*>,F7() by Th30;
then the Sorts of F6() tolerates the Sorts of (1GateCircuit <*F1(),F2()*>,F7()) by CIRCCOMB:def 3;
then reconsider s1 = (Following s,(stabilization-time s9)) | the carrier of (1GateCircStr <*F1(),F2()*>,F7()) as State of (1GateCircuit <*F1(),F2()*>,F7()) by CIRCCOMB:33;