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
; 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
; ( 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:127;
hence
InputVertices S = {F1(),F2()}
by CIRCCOMB:42; for s being State of A holds (Result s) . (Output S) = F4((s . F1()),(s . F2()))
let s be State of A; (Result s) . (Output S) = F4((s . F1()),(s . F2()))
reconsider sx = s * <*F1(),F2()*> as Element of 2 -tuples_on F3() by Th12;
A2:
dom <*F1(),F2()*> = Seg 2
by FINSEQ_1:89;
then A3:
1 in dom <*F1(),F2()*>
by FINSEQ_1:1;
A4:
2 in dom <*F1(),F2()*>
by A2, FINSEQ_1:1;
Result s = Following s
by Th20;
hence (Result s) . (Output S) =
(Following s) . [<*F1(),F2()*>,g]
by Th15
.=
g . (s * <*F1(),F2()*>)
by CIRCCOMB:56
.=
F4((sx . 1),(sx . 2))
by A1
.=
F4((s . (<*F1(),F2()*> . 1)),(sx . 2))
by A3, FUNCT_1:13
.=
F4((s . (<*F1(),F2()*> . 1)),(s . (<*F1(),F2()*> . 2)))
by A4, FUNCT_1:13
.=
F4((s . F1()),(s . (<*F1(),F2()*> . 2)))
by FINSEQ_1:44
.=
F4((s . F1()),(s . F2()))
by FINSEQ_1:44
;
verum