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