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 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 ;
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 ;
:: according to PBOOLE:def 18 :: thesis: ( 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 )
;
:: thesis: 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 X' =
X as
SetWithCompoundTerm of
S,
V by Th3;
reconsider g =
i as
Gate of
(X' -CircuitStr ) by A7;
A8:
the_result_sort_of g = g
by FUNCT_1:35;
then reconsider v =
g as
Vertex of
(X' -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 &
y in {the carrier of S} &
I . {} = [o,y] )
by ZFMISC_1:103;
reconsider o =
o as
OperSymbol of
S by A9;
A10:
o = (I . {} ) `1
by A9, MCART_1:7;
A11:
(
y = the
carrier of
S &
g . {} = [o,y] )
by A9, TARSKI:def 1;
ex
g being
Gate of
(X -CircuitStr ) st
(
g = i &
CHARACT . i = the_action_of g,
A )
by A5, A7;
then A12:
CHARACT . i =
the_action_of g,
A
.=
the
Charact of
A . o
by A10, Def3
;
A13:
(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, MSATERM:17
;
A14:
((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
;
A15:
(((X -CircuitSorts A) # ) * the Arity of (X -CircuitStr )) . g =
((X -CircuitSorts A) # ) . (the_arity_of g)
by FUNCT_2:21
.=
product ((X' -CircuitSorts A) * (the_arity_of g))
by PBOOLE:def 19
.=
product (the Sorts of A * (the_arity_of o))
by A11, 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 A12, A13, A14, A15, PBOOLE:def 18;
:: thesis: 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
; :: thesis: 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 ); :: thesis: ( g in the carrier' of (X -CircuitStr ) implies CHARACT . g = the_action_of g,A )
assume
g in the carrier' of (X -CircuitStr )
; :: thesis: 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
; :: thesis: verum