deffunc H1( Element of 2 -tuples_on F3()) -> Element of F3() = F4(($1 . 1),($1 . 2));
consider g being Function of (2 -tuples_on F3()),F3() such that
A1:
for a being Element of 2 -tuples_on F3() holds g . a = H1(a)
from FUNCT_2:sch 4();
reconsider S = 1GateCircStr <*F1(),F2()*>,g as one-gate ManySortedSign ;
take
S
; :: thesis: ex A being one-gate Circuit of S st
( InputVertices S = {F1(),F2()} & ( for s being State of A holds (Result s) . (Output S) = F4((s . F1()),(s . F2())) ) )
reconsider A = 1GateCircuit <*F1(),F2()*>,g as one-gate Circuit of S ;
take
A
; :: thesis: ( InputVertices S = {F1(),F2()} & ( for s being State of A holds (Result s) . (Output S) = F4((s . F1()),(s . F2())) ) )
rng <*F1(),F2()*> = {F1(),F2()}
by FINSEQ_2:147;
hence
InputVertices S = {F1(),F2()}
by CIRCCOMB:49; :: thesis: for s being State of A holds (Result s) . (Output S) = F4((s . F1()),(s . F2()))
let s be State of A; :: thesis: (Result s) . (Output S) = F4((s . F1()),(s . F2()))
reconsider sx = s * <*F1(),F2()*> as Element of 2 -tuples_on F3() by Th13;
dom <*F1(),F2()*> = Seg 2
by FINSEQ_3:29;
then A2:
( 1 in dom <*F1(),F2()*> & 2 in dom <*F1(),F2()*> )
by FINSEQ_1:3;
Result s = Following s
by Th21;
hence (Result s) . (Output S) =
(Following s) . [<*F1(),F2()*>,g]
by Th16
.=
g . (s * <*F1(),F2()*>)
by CIRCCOMB:64
.=
F4((sx . 1),(sx . 2))
by A1
.=
F4((s . (<*F1(),F2()*> . 1)),(sx . 2))
by A2, FUNCT_1:23
.=
F4((s . (<*F1(),F2()*> . 1)),(s . (<*F1(),F2()*> . 2)))
by A2, FUNCT_1:23
.=
F4((s . F1()),(s . (<*F1(),F2()*> . 2)))
by FINSEQ_1:61
.=
F4((s . F1()),(s . F2()))
by FINSEQ_1:61
;
:: thesis: verum