defpred S1[ set , set ] means ex g being Gate of (X -CircuitStr) st
( g = $1 & $2 = the_action_of (g,A) );
consider CHARACT being ManySortedSet of the carrier' of (X -CircuitStr) such that
A5:
for x being set st x in the carrier' of (X -CircuitStr) holds
S1[x,CHARACT . x]
from PBOOLE:sch 3(A4);
A6:
dom CHARACT = the carrier' of (X -CircuitStr)
by PARTFUN1:def 4;
CHARACT is Function-yielding
then reconsider CHARACT = CHARACT as ManySortedFunction of the carrier' of (X -CircuitStr) ;
CHARACT is ManySortedFunction of ((X -CircuitSorts A) #) * the Arity of (X -CircuitStr),(X -CircuitSorts A) * the ResultSort of (X -CircuitStr)
proof
let i be
set ;
PBOOLE:def 18 ( not i in the carrier' of (X -CircuitStr) or CHARACT . i is Element of bool [:((((X -CircuitSorts A) #) * the Arity of (X -CircuitStr)) . i),(((X -CircuitSorts A) * the ResultSort of (X -CircuitStr)) . i):] )
assume A7:
i in the
carrier' of
(X -CircuitStr)
;
CHARACT . i is Element of bool [:((((X -CircuitSorts A) #) * the Arity of (X -CircuitStr)) . i),(((X -CircuitSorts A) * the ResultSort of (X -CircuitStr)) . i):]
then
not
X -CircuitStr is
void
;
then reconsider X9 =
X as
SetWithCompoundTerm of
S,
V by Th3;
reconsider g =
i as
Gate of
(X9 -CircuitStr) by A7;
A8:
the_result_sort_of g = g
by FUNCT_1:35;
then reconsider v =
g as
Vertex of
(X9 -CircuitStr) ;
reconsider I =
i as
CompoundTerm of
S,
V by A7, Th4;
I . {} in [: the carrier' of S,{ the carrier of S}:]
by MSATERM:def 6;
then consider o,
y being
set such that A9:
o in the
carrier' of
S
and A10:
y in { the carrier of S}
and A11:
I . {} = [o,y]
by ZFMISC_1:103;
reconsider o =
o as
OperSymbol of
S by A9;
A12:
o = (I . {}) `1
by A11, MCART_1:7;
A13:
y = the
carrier of
S
by A10, TARSKI:def 1;
ex
g being
Gate of
(X -CircuitStr) st
(
g = i &
CHARACT . i = the_action_of (
g,
A) )
by A5, A7;
then A14:
CHARACT . i =
the_action_of (
g,
A)
.=
the
Charact of
A . o
by A12, Def3
;
A15:
( the Sorts of A * the ResultSort of S) . o =
the
Sorts of
A . (the_result_sort_of o)
by FUNCT_2:21
.=
the
Sorts of
A . (the_sort_of I)
by A11, A13, MSATERM:17
;
A16:
((X -CircuitSorts A) * the ResultSort of (X -CircuitStr)) . g =
(X -CircuitSorts A) . (the_result_sort_of g)
by FUNCT_2:21
.=
the_sort_of (
v,
A)
by A8, Def4
.=
the
Sorts of
A . (the_sort_of I)
by Def2
;
A17:
(((X -CircuitSorts A) #) * the Arity of (X -CircuitStr)) . g =
((X -CircuitSorts A) #) . (the_arity_of g)
by FUNCT_2:21
.=
product ((X9 -CircuitSorts A) * (the_arity_of g))
by PBOOLE:def 19
.=
product ( the Sorts of A * (the_arity_of o))
by A11, A13, Th14
;
(( the Sorts of A #) * the Arity of S) . o =
( the Sorts of A #) . (the_arity_of o)
by FUNCT_2:21
.=
product ( the Sorts of A * (the_arity_of o))
by PBOOLE:def 19
;
hence
CHARACT . i is
Element of
bool [:((((X -CircuitSorts A) #) * the Arity of (X -CircuitStr)) . i),(((X -CircuitSorts A) * the ResultSort of (X -CircuitStr)) . i):]
by A14, A15, A16, A17, PBOOLE:def 18;
verum
end;
then reconsider CHARACT = CHARACT as ManySortedFunction of ((X -CircuitSorts A) #) * the Arity of (X -CircuitStr),(X -CircuitSorts A) * the ResultSort of (X -CircuitStr) ;
take
CHARACT
; for g being Gate of (X -CircuitStr) st g in the carrier' of (X -CircuitStr) holds
CHARACT . g = the_action_of (g,A)
let g be Gate of (X -CircuitStr); ( g in the carrier' of (X -CircuitStr) implies CHARACT . g = the_action_of (g,A) )
assume
g in the carrier' of (X -CircuitStr)
; CHARACT . g = the_action_of (g,A)
then
ex h being Gate of (X -CircuitStr) st
( h = g & CHARACT . g = the_action_of (h,A) )
by A5;
hence
CHARACT . g = the_action_of (g,A)
; verum