let U be non empty set ; for u being Element of U
for k being Nat
for S being Language
for E being Equivalence_Relation of U
for I being b3,U -interpreter-like b4 -respecting Function holds (((I quotient E),((E -class) . u)) -TermEval) . k = (E -class) * (((I,u) -TermEval) . k)
let u be Element of U; for k being Nat
for S being Language
for E being Equivalence_Relation of U
for I being b2,U -interpreter-like b3 -respecting Function holds (((I quotient E),((E -class) . u)) -TermEval) . k = (E -class) * (((I,u) -TermEval) . k)
let k be Nat; for S being Language
for E being Equivalence_Relation of U
for I being b1,U -interpreter-like b2 -respecting Function holds (((I quotient E),((E -class) . u)) -TermEval) . k = (E -class) * (((I,u) -TermEval) . k)
let S be Language; for E being Equivalence_Relation of U
for I being S,U -interpreter-like b1 -respecting Function holds (((I quotient E),((E -class) . u)) -TermEval) . k = (E -class) * (((I,u) -TermEval) . k)
let E be Equivalence_Relation of U; for I being S,U -interpreter-like E -respecting Function holds (((I quotient E),((E -class) . u)) -TermEval) . k = (E -class) * (((I,u) -TermEval) . k)
reconsider e = (E -class) . u as Element of Class E ;
let I be S,U -interpreter-like E -respecting Function; (((I quotient E),((E -class) . u)) -TermEval) . k = (E -class) * (((I,u) -TermEval) . k)
set te = (I,u) -TermEval ;
set II = I quotient E;
set TE = ((I quotient E),e) -TermEval ;
set F = S -firstChar ;
set O = OwnSymbolsOf S;
set TT = AllTermsOf S;
defpred S1[ Nat] means (((I quotient E),e) -TermEval) . $1 = (E -class) * (((I,u) -TermEval) . $1);
A1:
S1[ 0 ]
A3:
for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be
Nat;
( S1[m] implies S1[m + 1] )
assume A4:
S1[
m]
;
S1[m + 1]
reconsider mm =
m,
MM =
m + 1 as
Element of
NAT by ORDINAL1:def 12;
(
((I,u) -TermEval) . mm is
Element of
Funcs (
(AllTermsOf S),
U) &
((I,u) -TermEval) . MM is
Element of
Funcs (
(AllTermsOf S),
U) )
;
then reconsider tm =
((I,u) -TermEval) . mm,
tmm =
((I,u) -TermEval) . MM as
Function of
(AllTermsOf S),
U ;
(
(((I quotient E),e) -TermEval) . mm is
Element of
Funcs (
(AllTermsOf S),
(Class E)) &
(((I quotient E),e) -TermEval) . MM is
Element of
Funcs (
(AllTermsOf S),
(Class E)) )
;
then reconsider TM =
(((I quotient E),e) -TermEval) . mm,
TMM =
(((I quotient E),e) -TermEval) . MM as
Function of
(AllTermsOf S),
(Class E) ;
now for tt being Element of AllTermsOf S holds TMM . tt = ((E -class) * tmm) . ttlet tt be
Element of
AllTermsOf S;
TMM . tt = ((E -class) * tmm) . ttreconsider t =
tt as
termal string of
S ;
set s =
(S -firstChar) . t;
set g =
I . ((S -firstChar) . t);
set G =
(I quotient E) . ((S -firstChar) . t);
set sub =
SubTerms t;
set n =
|.(ar ((S -firstChar) . t)).|;
reconsider gg =
I . ((S -firstChar) . t) as
|.(ar ((S -firstChar) . t)).| -placesOf E,
E -respecting Function of
(|.(ar ((S -firstChar) . t)).| -tuples_on U),
U by FOMODEL2:def 2;
A5:
(I . ((S -firstChar) . t)) quotient E = (gg quotient ((|.(ar ((S -firstChar) . t)).| -placesOf E),E)) * (|.(ar ((S -firstChar) . t)).| -tuple2Class E)
by Def15;
reconsider ggg =
gg quotient (
(|.(ar ((S -firstChar) . t)).| -placesOf E),
E) as
Function ;
A6:
(
tm * (SubTerms t) is
U -valued |.(ar ((S -firstChar) . t)).| -element FinSequence &
dom (|.(ar ((S -firstChar) . t)).| -placesOf (E -class)) = |.(ar ((S -firstChar) . t)).| -tuples_on U &
dom gg = |.(ar ((S -firstChar) . t)).| -tuples_on U &
dom tmm = AllTermsOf S )
by FUNCT_2:def 1;
thus TMM . tt =
((I quotient E) . ((S -firstChar) . t)) . (((((I quotient E),e) -TermEval) . m) * (SubTerms t))
by FOMODEL2:3
.=
((I . ((S -firstChar) . t)) quotient E) . (((((I quotient E),e) -TermEval) . m) * (SubTerms t))
by Def18
.=
((I . ((S -firstChar) . t)) quotient E) . ((E -class) * (tm * (SubTerms t)))
by RELAT_1:36, A4
.=
((I . ((S -firstChar) . t)) quotient E) . ((|.(ar ((S -firstChar) . t)).| -placesOf (E -class)) . (tm * (SubTerms t)))
by Lm19
.=
((ggg * (|.(ar ((S -firstChar) . t)).| -tuple2Class E)) * (|.(ar ((S -firstChar) . t)).| -placesOf (E -class))) . (tm * (SubTerms t))
by A5, A6, FOMODEL0:16, FUNCT_1:13
.=
(ggg * ((|.(ar ((S -firstChar) . t)).| -tuple2Class E) * (|.(ar ((S -firstChar) . t)).| -placesOf (E -class)))) . (tm * (SubTerms t))
by RELAT_1:36
.=
(ggg * ((|.(ar ((S -firstChar) . t)).| -placesOf E) -class)) . (tm * (SubTerms t))
by Lm20
.=
((E -class) * gg) . (tm * (SubTerms t))
by Lm18
.=
(E -class) . (gg . (tm * (SubTerms t)))
by A6, FOMODEL0:16, FUNCT_1:13
.=
(E -class) . ((((I,u) -TermEval) . (m + 1)) . t)
by FOMODEL2:3
.=
((E -class) * tmm) . tt
by A6, FUNCT_1:13
;
verum end;
hence
S1[
m + 1]
by FUNCT_2:63;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A3);
hence
(((I quotient E),((E -class) . u)) -TermEval) . k = (E -class) * (((I,u) -TermEval) . k)
; verum