let S be non empty non void ManySortedSign ; for V being V2() ManySortedSet of the carrier of S
for A being non-empty MSAlgebra over S
for X being SetWithCompoundTerm of S,V
for g being Gate of (X -CircuitStr)
for o being OperSymbol of S st g . {} = [o, the carrier of S] holds
(X -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o)
let V be V2() ManySortedSet of the carrier of S; for A being non-empty MSAlgebra over S
for X being SetWithCompoundTerm of S,V
for g being Gate of (X -CircuitStr)
for o being OperSymbol of S st g . {} = [o, the carrier of S] holds
(X -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o)
let A be non-empty MSAlgebra over S; for X being SetWithCompoundTerm of S,V
for g being Gate of (X -CircuitStr)
for o being OperSymbol of S st g . {} = [o, the carrier of S] holds
(X -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o)
let t be SetWithCompoundTerm of S,V; for g being Gate of (t -CircuitStr)
for o being OperSymbol of S st g . {} = [o, the carrier of S] holds
(t -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o)
let g be Gate of (t -CircuitStr); for o being OperSymbol of S st g . {} = [o, the carrier of S] holds
(t -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o)
set X = t;
reconsider f = g as CompoundTerm of S,V by Th4;
reconsider ag = the_arity_of g as FinSequence of Subtrees t ;
A1:
g = (f . {}) -tree ag
by Th12;
let o be OperSymbol of S; ( g . {} = [o, the carrier of S] implies (t -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o) )
assume
g . {} = [o, the carrier of S]
; (t -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o)
then consider a being ArgumentSeq of Sym (o,V) such that
A2:
f = [o, the carrier of S] -tree a
by MSATERM:10;
A3:
len a = len (the_arity_of o)
by MSATERM:22;
A4:
a = ag
by A1, A2, TREES_4:15;
A5:
dom (the_arity_of o) = Seg (len a)
by A3, FINSEQ_1:def 3;
A6:
dom (the_arity_of g) = Seg (len a)
by A4, FINSEQ_1:def 3;
A7:
rng (the_arity_of g) c= the carrier of (t -CircuitStr)
by FINSEQ_1:def 4;
A8:
rng (the_arity_of o) c= the carrier of S
by FINSEQ_1:def 4;
A9:
dom (t -CircuitSorts A) = the carrier of (t -CircuitStr)
by PARTFUN1:def 2;
A10:
dom the Sorts of A = the carrier of S
by PARTFUN1:def 2;
A11:
dom ((t -CircuitSorts A) * (the_arity_of g)) = Seg (len a)
by A6, A7, A9, RELAT_1:27;
A12:
dom ( the Sorts of A * (the_arity_of o)) = Seg (len a)
by A5, A8, A10, RELAT_1:27;
now for i being object st i in Seg (len a) holds
((t -CircuitSorts A) * (the_arity_of g)) . i = ( the Sorts of A * (the_arity_of o)) . ilet i be
object ;
( i in Seg (len a) implies ((t -CircuitSorts A) * (the_arity_of g)) . i = ( the Sorts of A * (the_arity_of o)) . i )assume A13:
i in Seg (len a)
;
((t -CircuitSorts A) * (the_arity_of g)) . i = ( the Sorts of A * (the_arity_of o)) . ithen reconsider j =
i as
Element of
NAT ;
ag . i in rng (the_arity_of g)
by A6, A13, FUNCT_1:def 3;
then reconsider v =
ag . j as
Vertex of
(t -CircuitStr) by A7;
(the_arity_of o) . i in rng (the_arity_of o)
by A5, A13, FUNCT_1:def 3;
then reconsider s =
(the_arity_of o) . j as
SortSymbol of
S by A8;
reconsider u =
v as
Term of
S,
V by A4, A6, A13, MSATERM:22;
A14:
the_sort_of u = s
by A4, A6, A13, MSATERM:23;
A15:
((t -CircuitSorts A) * (the_arity_of g)) . i = (t -CircuitSorts A) . v
by A11, A13, FUNCT_1:12;
A16:
( the Sorts of A * (the_arity_of o)) . i = the
Sorts of
A . s
by A12, A13, FUNCT_1:12;
thus ((t -CircuitSorts A) * (the_arity_of g)) . i =
the_sort_of (
v,
A)
by A15, Def4
.=
( the Sorts of A * (the_arity_of o)) . i
by A14, A16, Def2
;
verum end;
hence
(t -CircuitSorts A) * (the_arity_of g) = the Sorts of A * (the_arity_of o)
by A11, A12, FUNCT_1:2; verum