set S = 1GateCircStr (<*F1(),F2()*>,F7());
let s be State of (F6() +* (1GateCircuit (<*F1(),F2()*>,F7()))); 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(); ( 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()
; 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 Th16;
then A5:
InputVertices F5() misses InnerVertices (1GateCircStr (<*F1(),F2()*>,F7()))
by A2, ZFMISC_1:50;
then A6: (Following (s,(stabilization-time s9))) | the carrier of F5() =
Following (s9,(stabilization-time s9))
by A3, Th27, CIRCCMB2:13
.=
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(); ( ( 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() ) )
; (Result s) . (Output (1GateCircStr (<*F1(),F2()*>,F7()))) = F4(a1,a2)
A9:
InputVertices (1GateCircStr (<*F1(),F2()*>,F7())) = rng <*F1(),F2()*>
by CIRCCOMB:42;
F5() tolerates 1GateCircStr (<*F1(),F2()*>,F7())
by CIRCCOMB:47;
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:127;
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:49;
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:49;
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 XTUPLE_0:1
.=
the_arity_of g
by MSUALG_1:def 1
;
A17:
g `2 = F7()
;
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 Th15;
A21:
s is stabilizing
by Def2;
A22:
dom (Following (s,(stabilization-time s9))) = the carrier of (F5() +* (1GateCircStr (<*F1(),F2()*>,F7())))
by CIRCUIT1:3;
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:125;
A24: the_result_sort_of g =
the ResultSort of (F5() +* (1GateCircStr (<*F1(),F2()*>,F7()))) . 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 (<*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
;
verum