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