let S be Language; for U being non empty set
for I being S,b1 -interpreter-like Function
for xx being Function of (AllTermsOf S),U holds
( ^^^(I * (S -firstChar)),^^^xx,(S -subTerms)____ is Element of Funcs ((AllTermsOf S),U) & AllTermsOf S c= dom (I * (S -firstChar)) )
let U be non empty set ; for I being S,U -interpreter-like Function
for xx being Function of (AllTermsOf S),U holds
( ^^^(I * (S -firstChar)),^^^xx,(S -subTerms)____ is Element of Funcs ((AllTermsOf S),U) & AllTermsOf S c= dom (I * (S -firstChar)) )
let I be S,U -interpreter-like Function; for xx being Function of (AllTermsOf S),U holds
( ^^^(I * (S -firstChar)),^^^xx,(S -subTerms)____ is Element of Funcs ((AllTermsOf S),U) & AllTermsOf S c= dom (I * (S -firstChar)) )
set A = AllTermsOf S;
set F = S -firstChar ;
set ST = S -subTerms ;
set SS = AllSymbolsOf S;
set Z = AtomicTermsOf S;
set T = S -termsOfMaxDepth ;
A1:
dom (S -firstChar) = ((AllSymbolsOf S) *) \ {{}}
by FUNCT_2:def 1;
let xx be Function of (AllTermsOf S),U; ( ^^^(I * (S -firstChar)),^^^xx,(S -subTerms)____ is Element of Funcs ((AllTermsOf S),U) & AllTermsOf S c= dom (I * (S -firstChar)) )
set f = ^^^xx,(S -subTerms)__;
set g = ^^^(I * (S -firstChar)),^^^xx,(S -subTerms)____;
A2: dom ^^^xx,(S -subTerms)__ =
dom (S -subTerms)
by Def6
.=
AllTermsOf S
by FUNCT_2:def 1
;
A3:
for a being set st a in AllTermsOf S holds
( a in dom (I * (S -firstChar)) & ( a in dom ^^^(I * (S -firstChar)),^^^xx,(S -subTerms)____ implies ^^^(I * (S -firstChar)),^^^xx,(S -subTerms)____ . a in U ) )
proof
let a be
set ;
( a in AllTermsOf S implies ( a in dom (I * (S -firstChar)) & ( a in dom ^^^(I * (S -firstChar)),^^^xx,(S -subTerms)____ implies ^^^(I * (S -firstChar)),^^^xx,(S -subTerms)____ . a in U ) ) )
assume A4:
a in AllTermsOf S
;
( a in dom (I * (S -firstChar)) & ( a in dom ^^^(I * (S -firstChar)),^^^xx,(S -subTerms)____ implies ^^^(I * (S -firstChar)),^^^xx,(S -subTerms)____ . a in U ) )
then reconsider t =
a as
termal string of
S ;
set n =
|.(ar t).|;
reconsider ss =
(S -firstChar) . t as
termal Element of
S ;
reconsider s =
ss as
own Element of
S ;
reconsider t1 =
s as
Element of
OwnSymbolsOf S by FOMODEL1:def 19;
(
t1 in OwnSymbolsOf S &
OwnSymbolsOf S c= dom I )
by Lm2;
hence A5:
a in dom (I * (S -firstChar))
by FUNCT_1:11, A1;
( a in dom ^^^(I * (S -firstChar)),^^^xx,(S -subTerms)____ implies ^^^(I * (S -firstChar)),^^^xx,(S -subTerms)____ . a in U )
reconsider tt =
a as
Element of
AllTermsOf S by A4;
reconsider i =
I . s as
Interpreter of
s,
U ;
(S -subTerms) . tt = SubTerms t
by FOMODEL1:def 39;
then reconsider y =
(S -subTerms) . tt as
|.(ar t).| -element FinSequence of
AllTermsOf S by FINSEQ_1:def 11;
reconsider z =
xx * y as
|.(ar t).| -element FinSequence of
U ;
len z = |.(ar t).|
by CARD_1:def 7;
then reconsider zz =
z as
Element of
|.(ar t).| -tuples_on U by FINSEQ_2:133;
|.(ar t).| -tuples_on U c= dom (I . t1)
by Lm3;
then A6:
zz in dom i
;
tt in AllTermsOf S
;
then A7:
tt in dom (S -subTerms)
by FUNCT_2:def 1;
assume
a in dom ^^^(I * (S -firstChar)),^^^xx,(S -subTerms)____
;
^^^(I * (S -firstChar)),^^^xx,(S -subTerms)____ . a in U
then ^^^(I * (S -firstChar)),^^^xx,(S -subTerms)____ . t =
((I * (S -firstChar)) . t) . (^^^xx,(S -subTerms)__ . t)
by FOMODEL0:def 4
.=
(I . s) . (^^^xx,(S -subTerms)__ . t)
by A5, FUNCT_1:12
.=
i . zz
by Def6, A7
;
hence
^^^(I * (S -firstChar)),^^^xx,(S -subTerms)____ . a in U
by A6, FUNCT_1:102;
verum
end;
then A8:
for a being object st a in AllTermsOf S holds
a in dom (I * (S -firstChar))
;
A9: dom ^^^(I * (S -firstChar)),^^^xx,(S -subTerms)____ =
(dom (I * (S -firstChar))) /\ (AllTermsOf S)
by A2, FOMODEL0:def 4
.=
AllTermsOf S
by A8, TARSKI:def 3, XBOOLE_1:28
;
then
for a being object st a in AllTermsOf S holds
^^^(I * (S -firstChar)),^^^xx,(S -subTerms)____ . a in U
by A3;
then
^^^(I * (S -firstChar)),^^^xx,(S -subTerms)____ is Function of (AllTermsOf S),U
by FUNCT_2:3, A9;
hence
^^^(I * (S -firstChar)),^^^xx,(S -subTerms)____ is Element of Funcs ((AllTermsOf S),U)
by FUNCT_2:8; AllTermsOf S c= dom (I * (S -firstChar))
thus
AllTermsOf S c= dom (I * (S -firstChar))
by A8; verum