let X be set ; for U being non empty set
for n being Nat
for S being Language
for l being literal Element of S
for I being b3,b1 -interpreter-like Function
for tt0 being Element of AllTermsOf S holds ((I -TermEval) * (((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . n)) | ((S -termsOfMaxDepth) . n) = (((((l,((I -TermEval) . tt0)) ReassignIn I),((I -TermEval) . tt0)) -TermEval) . n) | ((S -termsOfMaxDepth) . n)
let U be non empty set ; for n being Nat
for S being Language
for l being literal Element of S
for I being b2,U -interpreter-like Function
for tt0 being Element of AllTermsOf S holds ((I -TermEval) * (((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . n)) | ((S -termsOfMaxDepth) . n) = (((((l,((I -TermEval) . tt0)) ReassignIn I),((I -TermEval) . tt0)) -TermEval) . n) | ((S -termsOfMaxDepth) . n)
let n be Nat; for S being Language
for l being literal Element of S
for I being b1,U -interpreter-like Function
for tt0 being Element of AllTermsOf S holds ((I -TermEval) * (((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . n)) | ((S -termsOfMaxDepth) . n) = (((((l,((I -TermEval) . tt0)) ReassignIn I),((I -TermEval) . tt0)) -TermEval) . n) | ((S -termsOfMaxDepth) . n)
let S be Language; for l being literal Element of S
for I being S,U -interpreter-like Function
for tt0 being Element of AllTermsOf S holds ((I -TermEval) * (((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . n)) | ((S -termsOfMaxDepth) . n) = (((((l,((I -TermEval) . tt0)) ReassignIn I),((I -TermEval) . tt0)) -TermEval) . n) | ((S -termsOfMaxDepth) . n)
let l be literal Element of S; for I being S,U -interpreter-like Function
for tt0 being Element of AllTermsOf S holds ((I -TermEval) * (((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . n)) | ((S -termsOfMaxDepth) . n) = (((((l,((I -TermEval) . tt0)) ReassignIn I),((I -TermEval) . tt0)) -TermEval) . n) | ((S -termsOfMaxDepth) . n)
let I be S,U -interpreter-like Function; for tt0 being Element of AllTermsOf S holds ((I -TermEval) * (((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . n)) | ((S -termsOfMaxDepth) . n) = (((((l,((I -TermEval) . tt0)) ReassignIn I),((I -TermEval) . tt0)) -TermEval) . n) | ((S -termsOfMaxDepth) . n)
let tt0 be Element of AllTermsOf S; ((I -TermEval) * (((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . n)) | ((S -termsOfMaxDepth) . n) = (((((l,((I -TermEval) . tt0)) ReassignIn I),((I -TermEval) . tt0)) -TermEval) . n) | ((S -termsOfMaxDepth) . n)
set II = U -InterpretersOf S;
reconsider u = (I -TermEval) . tt0 as Element of U ;
set F = S -firstChar ;
set FI = (S,X) -freeInterpreter ;
set H = (l,tt0) ReassignIn ((S,X) -freeInterpreter);
set TT = AllTermsOf S;
set TI = (I,u) -TermEval ;
set TF = (((S,X) -freeInterpreter),tt0) -TermEval ;
set TH = (((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval ;
set TII = I -TermEval ;
set J = (l,((I -TermEval) . tt0)) ReassignIn I;
set TJ = (((l,((I -TermEval) . tt0)) ReassignIn I),u) -TermEval ;
set C = S -multiCat ;
set SS = AllSymbolsOf S;
set T = S -termsOfMaxDepth ;
reconsider t0 = tt0 as termal string of S ;
set k = Depth t0;
reconsider t00 = t0 as Depth t0 -termal string of S by FOMODEL1:def 40;
A1:
( l in {l} & dom (l .--> ({} .--> tt0)) = {l} & dom (l .--> ({} .--> ((I -TermEval) . tt0))) = {l} )
by TARSKI:def 1;
then
( ((l,tt0) ReassignIn ((S,X) -freeInterpreter)) . l = (l .--> ({} .--> tt0)) . l & ((l,((I -TermEval) . tt0)) ReassignIn I) . l = (l .--> ({} .--> ((I -TermEval) . tt0))) . l )
by FUNCT_4:13;
then A2:
( ((l,tt0) ReassignIn ((S,X) -freeInterpreter)) . l = {} .--> tt0 & ((l,((I -TermEval) . tt0)) ReassignIn I) . l = {} .--> ((I -TermEval) . tt0) )
by A1, FUNCOP_1:7;
defpred S1[ Nat] means ((I -TermEval) * (((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . $1)) | ((S -termsOfMaxDepth) . $1) = (((((l,((I -TermEval) . tt0)) ReassignIn I),u) -TermEval) . $1) | ((S -termsOfMaxDepth) . $1);
A3:
S1[ 0 ]
proof
A4:
(
dom ((AllTermsOf S) --> u) = AllTermsOf S &
dom ((AllTermsOf S) --> tt0) = AllTermsOf S &
dom (I -TermEval) = AllTermsOf S )
by FUNCT_2:def 1;
(
((I,u) -TermEval) . 0 = (AllTermsOf S) --> u &
((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . 0 = (AllTermsOf S) --> tt0 )
by FOMODEL2:def 8;
then (I -TermEval) * (((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . 0) =
(AllTermsOf S) --> ((I -TermEval) . tt0)
by FUNCOP_1:17, A4
.=
((((l,((I -TermEval) . tt0)) ReassignIn I),u) -TermEval) . 0
by FOMODEL2:def 8
;
hence
S1[
0 ]
;
verum
end;
A5:
for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be
Nat;
( S1[m] implies S1[m + 1] )
reconsider mm =
m,
MM =
m + 1 as
Element of
NAT by ORDINAL1:def 12;
assume A6:
S1[
m]
;
S1[m + 1]
reconsider TM =
(S -termsOfMaxDepth) . MM,
Tm =
(S -termsOfMaxDepth) . mm as
Subset of
(AllTermsOf S) by FOMODEL1:2;
(
((((l,((I -TermEval) . tt0)) ReassignIn I),u) -TermEval) . mm is
Element of
Funcs (
(AllTermsOf S),
U) &
((I,u) -TermEval) . MM is
Element of
Funcs (
(AllTermsOf S),
U) &
((((l,((I -TermEval) . tt0)) ReassignIn I),u) -TermEval) . MM is
Element of
Funcs (
(AllTermsOf S),
U) &
((I,u) -TermEval) . mm is
Element of
Funcs (
(AllTermsOf S),
U) )
;
then reconsider Jm =
((((l,((I -TermEval) . tt0)) ReassignIn I),u) -TermEval) . mm,
JM =
((((l,((I -TermEval) . tt0)) ReassignIn I),u) -TermEval) . MM,
IM =
((I,u) -TermEval) . MM,
Imm =
((I,u) -TermEval) . mm as
Function of
(AllTermsOf S),
U ;
(
((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . mm is
Element of
Funcs (
(AllTermsOf S),
(AllTermsOf S)) &
((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . MM is
Element of
Funcs (
(AllTermsOf S),
(AllTermsOf S)) )
;
then reconsider Hm =
((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . mm,
HM =
((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . MM as
Function of
(AllTermsOf S),
(AllTermsOf S) ;
set LH =
((I -TermEval) * HM) | TM;
set RH =
JM | TM;
A7:
(
dom (((I -TermEval) * HM) | TM) = TM &
dom (JM | TM) = TM )
by PARTFUN1:def 2;
now for x being object st x in dom (((I -TermEval) * HM) | TM) holds
(((I -TermEval) * HM) | TM) . x = (JM | TM) . xlet x be
object ;
( x in dom (((I -TermEval) * HM) | TM) implies (((I -TermEval) * HM) | TM) . b1 = (JM | TM) . b1 )assume A8:
x in dom (((I -TermEval) * HM) | TM)
;
(((I -TermEval) * HM) | TM) . b1 = (JM | TM) . b1then reconsider tt =
x as
Element of
AllTermsOf S by A7;
reconsider t =
x as
mm + 1
-termal string of
S by A7, FOMODEL1:def 33, A8;
reconsider ttt =
x as
Element of
TM by A8;
set ST =
SubTerms t;
set o =
(S -firstChar) . t;
set n =
|.(ar ((S -firstChar) . t)).|;
(
(((IM * HM) | TM) . ttt) \+\ ((IM * HM) . ttt) = {} &
((JM | TM) . ttt) \+\ (JM . ttt) = {} &
((((I -TermEval) * HM) | TM) . ttt) \+\ (((I -TermEval) * HM) . ttt) = {} )
;
then A9:
(
((IM * HM) | TM) . x = (IM * HM) . x &
(JM | TM) . x = JM . x &
(((I -TermEval) * HM) | TM) . x = ((I -TermEval) * HM) . x )
by FOMODEL0:29;
(
((IM * HM) . tt) \+\ (IM . (HM . tt)) = {} &
(((I -TermEval) * HM) . tt) \+\ ((I -TermEval) . (HM . tt)) = {} )
;
then A10:
(
(IM * HM) . t = IM . (HM . t) &
((I -TermEval) * HM) . tt = (I -TermEval) . (HM . tt) )
by FOMODEL0:29;
reconsider newterms =
Hm * (SubTerms t) as
|.(ar ((S -firstChar) . t)).| -element FinSequence of
AllTermsOf S by FOMODEL0:26;
reconsider newtermss =
newterms as
Element of
|.(ar ((S -firstChar) . t)).| -tuples_on (AllTermsOf S) by FOMODEL0:16;
reconsider newtermsss =
newterms as
FinSequence of
((AllSymbolsOf S) *) \ {{}} by FOMODEL0:26;
(((((S -firstChar) . t) -compound) | (|.(ar ((S -firstChar) . t)).| -tuples_on (AllTermsOf S))) . newtermss) \+\ ((((S -firstChar) . t) -compound) . newtermss) = {}
;
then A11:
((((S -firstChar) . t) -compound) | (|.(ar ((S -firstChar) . t)).| -tuples_on (AllTermsOf S))) . newterms = (((S -firstChar) . t) -compound) . newterms
by FOMODEL0:29;
per cases
( (S -firstChar) . t = l or (S -firstChar) . t <> l )
;
suppose
(S -firstChar) . t <> l
;
(((I -TermEval) * HM) | TM) . b1 = (JM | TM) . b1then A12:
( not
(S -firstChar) . t in dom (l .--> ({} .--> tt0)) & not
(S -firstChar) . t in dom (l .--> ({} .--> ((I -TermEval) . tt0))) )
by TARSKI:def 1;
then
((S,X) -freeInterpreter) . ((S -firstChar) . t) = ((l,tt0) ReassignIn ((S,X) -freeInterpreter)) . ((S -firstChar) . t)
by FUNCT_4:11;
then ((l,tt0) ReassignIn ((S,X) -freeInterpreter)) . ((S -firstChar) . t) =
X -freeInterpreter ((S -firstChar) . t)
by Def4
.=
(((S -firstChar) . t) -compound) | (|.(ar ((S -firstChar) . t)).| -tuples_on (AllTermsOf S))
by Def3
;
then A13:
(((l,tt0) ReassignIn ((S,X) -freeInterpreter)) . ((S -firstChar) . t)) . newterms = ((S -firstChar) . t) -compound newtermsss
by A11, Def2;
reconsider newtermssss =
newterms as
|.(ar ((S -firstChar) . t)).| -element Element of
(AllTermsOf S) * ;
reconsider t1 =
((S -firstChar) . t) -compound newtermssss as
termal string of
S ;
set p =
Depth t1;
reconsider pp =
Depth t1 as
Element of
NAT by ORDINAL1:def 12;
reconsider t111 =
t1 as
Depth t1 -termal string of
S by FOMODEL1:def 40;
reconsider t11 =
t1 as
Element of
AllTermsOf S by FOMODEL1:def 32;
((I,u) -TermEval) . pp is
Element of
Funcs (
(AllTermsOf S),
U)
;
then reconsider Ip =
((I,u) -TermEval) . pp as
Function of
(AllTermsOf S),
U ;
A14:
(S -firstChar) . t1 =
t1 . 1
by FOMODEL0:6
.=
(S -firstChar) . t
by FINSEQ_1:41
;
then A15:
SubTerms t1 = newtermssss
by FOMODEL1:def 37;
A16:
(
dom (Hm | Tm) = Tm &
dom (Jm | Tm) = Tm &
rng (SubTerms t) c= Tm )
by RELAT_1:def 19, PARTFUN1:def 2;
((I -TermEval) * HM) . t =
(I -TermEval) . t1
by A13, FOMODEL2:3, A10
.=
(I . ((S -firstChar) . t)) . ((I -TermEval) * (SubTerms t1))
by A14, FOMODEL2:21
.=
(I . ((S -firstChar) . t)) . ((I -TermEval) * ((Hm | Tm) * (SubTerms t)))
by A16, RELAT_1:165, A15
.=
(I . ((S -firstChar) . t)) . (((I -TermEval) * (Hm | Tm)) * (SubTerms t))
by RELAT_1:36
.=
(I . ((S -firstChar) . t)) . ((((I -TermEval) * Hm) | Tm) * (SubTerms t))
by RELAT_1:83
.=
(I . ((S -firstChar) . t)) . (Jm * (SubTerms t))
by A6, A16, RELAT_1:165
.=
(((l,((I -TermEval) . tt0)) ReassignIn I) . ((S -firstChar) . t)) . (Jm * (SubTerms t))
by FUNCT_4:11, A12
.=
JM . t
by FOMODEL2:3
;
hence
(((I -TermEval) * HM) | TM) . x = (JM | TM) . x
by A9;
verum end; end;
hence
S1[
m + 1]
by A7, FUNCT_1:2;
verum
end;
for m being Nat holds S1[m]
from NAT_1:sch 2(A3, A5);
hence
((I -TermEval) * (((((l,tt0) ReassignIn ((S,X) -freeInterpreter)),tt0) -TermEval) . n)) | ((S -termsOfMaxDepth) . n) = (((((l,((I -TermEval) . tt0)) ReassignIn I),((I -TermEval) . tt0)) -TermEval) . n) | ((S -termsOfMaxDepth) . n)
; verum