let C be initialized ConstructorSignature; for c being constructor OperSymbol of C
for p being DTree-yielding FinSequence holds
( [c, the carrier of C] -tree p is expression of C iff ( len p = len (the_arity_of c) & p in (QuasiTerms C) * ) )
let c be constructor OperSymbol of C; for p being DTree-yielding FinSequence holds
( [c, the carrier of C] -tree p is expression of C iff ( len p = len (the_arity_of c) & p in (QuasiTerms C) * ) )
set o = c;
A1:
c <> *
by Def11;
A2:
c <> non_op
by Def11;
let p be DTree-yielding FinSequence; ( [c, the carrier of C] -tree p is expression of C iff ( len p = len (the_arity_of c) & p in (QuasiTerms C) * ) )
set V = (MSVars C) (\/) ( the carrier of C --> {0});
A3:
the Sorts of (Free (C,(MSVars C))) = C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0})))
by MSAFREE3:24;
hereby ( len p = len (the_arity_of c) & p in (QuasiTerms C) * implies [c, the carrier of C] -tree p is expression of C )
assume A4:
[c, the carrier of C] -tree p is
expression of
C
;
( len p = len (the_arity_of c) & p in (QuasiTerms C) * )then A5:
[c, the carrier of C] -tree p is
Term of
C,
((MSVars C) (\/) ( the carrier of C --> {0}))
by MSAFREE3:8;
then A6:
p is
ArgumentSeq of
Sym (
c,
((MSVars C) (\/) ( the carrier of C --> {0})))
by MSATERM:1;
hence
len p = len (the_arity_of c)
by MSATERM:22;
p in (QuasiTerms C) * reconsider q =
p as
ArgumentSeq of
Sym (
c,
((MSVars C) (\/) ( the carrier of C --> {0})))
by A5, MSATERM:1;
A7:
the_sort_of ((Sym (c,((MSVars C) (\/) ( the carrier of C --> {0})))) -tree q) = the_result_sort_of c
by MSATERM:20;
A8:
variables_in ((Sym (c,((MSVars C) (\/) ( the carrier of C --> {0})))) -tree q) c= MSVars C
by A4, MSAFREE3:27;
(C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0})))) . (the_result_sort_of c) = { t where t is Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) : ( the_sort_of t = the_result_sort_of c & variables_in t c= MSVars C ) }
by MSAFREE3:def 5;
then
(Sym (c,((MSVars C) (\/) ( the carrier of C --> {0})))) -tree p in (C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0})))) . (the_result_sort_of c)
by A7, A8;
then A9:
rng p c= Union (C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0}))))
by A6, MSAFREE3:19;
rng p c= QuasiTerms C
proof
let a be
object ;
TARSKI:def 3 ( not a in rng p or a in QuasiTerms C )
assume A10:
a in rng p
;
a in QuasiTerms C
then reconsider ta =
a as
expression of
C by A9, MSAFREE3:24;
consider i being
object such that A11:
i in dom p
and A12:
a = p . i
by A10, FUNCT_1:def 3;
reconsider i =
i as
Nat by A11;
reconsider t =
p . i as
Term of
C,
((MSVars C) (\/) ( the carrier of C --> {0})) by A6, A11, MSATERM:22;
A13:
the
Arity of
C . c in {a_Term} *
by A1, A2, Def9;
A14:
dom p = dom (the_arity_of c)
by A6, MSATERM:22;
A15:
the_arity_of c is
FinSequence of
{a_Term}
by A13, FINSEQ_1:def 11;
A16:
(the_arity_of c) . i in rng (the_arity_of c)
by A11, A14, FUNCT_1:def 3;
rng (the_arity_of c) c= {(a_Term C)}
by A15, FINSEQ_1:def 4;
then
(the_arity_of c) . i = a_Term C
by A16, TARSKI:def 1;
then A17:
the_sort_of t = a_Term C
by A6, A11, MSATERM:23;
t = ta
by A12;
then
variables_in t c= MSVars C
by MSAFREE3:27;
then
t in { T where T is Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) : ( the_sort_of T = a_Term C & variables_in T c= MSVars C ) }
by A17;
then
t in (C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0})))) . (a_Term C)
by MSAFREE3:def 5;
hence
a in QuasiTerms C
by A12, MSAFREE3:23;
verum
end; then
p is
FinSequence of
QuasiTerms C
by FINSEQ_1:def 4;
hence
p in (QuasiTerms C) *
by FINSEQ_1:def 11;
verum
end;
assume A18:
len p = len (the_arity_of c)
; ( not p in (QuasiTerms C) * or [c, the carrier of C] -tree p is expression of C )
assume A19:
p in (QuasiTerms C) *
; [c, the carrier of C] -tree p is expression of C
Free (C,(MSVars C)) = (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) | (C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0}))))
by MSAFREE3:25;
then
the Sorts of (Free (C,(MSVars C))) is ManySortedSubset of the Sorts of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0})))
by MSUALG_2:def 9;
then
the Sorts of (Free (C,(MSVars C))) c= the Sorts of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0})))
by PBOOLE:def 18;
then A20:
QuasiTerms C c= the Sorts of (FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) . (a_Term C)
;
A21:
p is FinSequence of QuasiTerms C
by A19, FINSEQ_1:def 11;
then A22:
rng p c= QuasiTerms C
by FINSEQ_1:def 4;
now for i being Nat st i in dom p holds
ex T being Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) st
( T = p . i & the_sort_of T = (the_arity_of c) . i )let i be
Nat;
( i in dom p implies ex T being Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) st
( T = p . i & the_sort_of T = (the_arity_of c) . i ) )assume A23:
i in dom p
;
ex T being Term of C,((MSVars C) (\/) ( the carrier of C --> {0})) st
( T = p . i & the_sort_of T = (the_arity_of c) . i )then
p . i in rng p
by FUNCT_1:def 3;
then A24:
p . i in QuasiTerms C
by A22;
then reconsider t =
p . i as
expression of
C ;
A25:
the
Arity of
C . c in {a_Term} *
by A1, A2, Def9;
A26:
dom p = dom (the_arity_of c)
by A18, FINSEQ_3:29;
A27:
the_arity_of c is
FinSequence of
{a_Term}
by A25, FINSEQ_1:def 11;
A28:
(the_arity_of c) . i in rng (the_arity_of c)
by A23, A26, FUNCT_1:def 3;
rng (the_arity_of c) c= {(a_Term C)}
by A27, FINSEQ_1:def 4;
then A29:
(the_arity_of c) . i = a_Term C
by A28, TARSKI:def 1;
reconsider T =
t as
Term of
C,
((MSVars C) (\/) ( the carrier of C --> {0})) by MSAFREE3:8;
take T =
T;
( T = p . i & the_sort_of T = (the_arity_of c) . i )thus
T = p . i
;
the_sort_of T = (the_arity_of c) . i
T in the
Sorts of
(FreeMSA ((MSVars C) (\/) ( the carrier of C --> {0}))) . (a_Term C)
by A20, A24;
then
T in FreeSort (
((MSVars C) (\/) ( the carrier of C --> {0})),
(a_Term C))
by MSAFREE:def 11;
hence
the_sort_of T = (the_arity_of c) . i
by A29, MSATERM:def 5;
verum end;
then A30:
p is ArgumentSeq of Sym (c,((MSVars C) (\/) ( the carrier of C --> {0})))
by A18, MSATERM:24;
A31:
dom the Sorts of (Free (C,(MSVars C))) = the carrier of C
by PARTFUN1:def 2;
rng p c= Union (C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0}))))
by A3, A21, FINSEQ_1:def 4;
then
(Sym (c,((MSVars C) (\/) ( the carrier of C --> {0})))) -tree p in (C -Terms ((MSVars C),((MSVars C) (\/) ( the carrier of C --> {0})))) . (the_result_sort_of c)
by A30, MSAFREE3:19;
hence
[c, the carrier of C] -tree p is expression of C
by A3, A31, CARD_5:2; verum