let U be non empty set ; for u being Element of U
for m being Nat
for S being Language
for l1, l2 being literal Element of S
for I being b3,U -interpreter-like Function holds (((l1,u) ReassignIn I) -TermEval) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m)) = ((((l2,u) ReassignIn I) -TermEval) * (l1 SubstWith l2)) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m))
let u be Element of U; for m being Nat
for S being Language
for l1, l2 being literal Element of S
for I being b2,U -interpreter-like Function holds (((l1,u) ReassignIn I) -TermEval) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m)) = ((((l2,u) ReassignIn I) -TermEval) * (l1 SubstWith l2)) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m))
let m be Nat; for S being Language
for l1, l2 being literal Element of S
for I being b1,U -interpreter-like Function holds (((l1,u) ReassignIn I) -TermEval) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m)) = ((((l2,u) ReassignIn I) -TermEval) * (l1 SubstWith l2)) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m))
let S be Language; for l1, l2 being literal Element of S
for I being S,U -interpreter-like Function holds (((l1,u) ReassignIn I) -TermEval) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m)) = ((((l2,u) ReassignIn I) -TermEval) * (l1 SubstWith l2)) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m))
let l1, l2 be literal Element of S; for I being S,U -interpreter-like Function holds (((l1,u) ReassignIn I) -TermEval) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m)) = ((((l2,u) ReassignIn I) -TermEval) * (l1 SubstWith l2)) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m))
let I be S,U -interpreter-like Function; (((l1,u) ReassignIn I) -TermEval) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m)) = ((((l2,u) ReassignIn I) -TermEval) * (l1 SubstWith l2)) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m))
set I1 = (l1,u) ReassignIn I;
set I2 = (l2,u) ReassignIn I;
set s = l1 SubstWith l2;
set E1 = ((l1,u) ReassignIn I) -TermEval ;
set E2 = ((l2,u) ReassignIn I) -TermEval ;
set T = S -termsOfMaxDepth ;
set TT = AllTermsOf S;
set SS = AllSymbolsOf S;
set F = S -firstChar ;
set C = S -multiCat ;
set g1 = l1 .--> ({} .--> u);
set g2 = l2 .--> ({} .--> u);
set L = LettersOf S;
reconsider SSS = (AllSymbolsOf S) \ {l2} as non empty Subset of (AllSymbolsOf S) ;
set D = SSS * ;
( l1 in {l1} & l2 in {l2} )
by TARSKI:def 1;
then
( l1 in dom (l1 .--> ({} .--> u)) & l2 in dom (l2 .--> ({} .--> u)) )
;
then
( ((l1,u) ReassignIn I) . l1 = (l1 .--> ({} .--> u)) . l1 & ((l2,u) ReassignIn I) . l2 = (l2 .--> ({} .--> u)) . l2 )
by FUNCT_4:13;
then A1:
( ((l1,u) ReassignIn I) . l1 = {} .--> u & ((l2,u) ReassignIn I) . l2 = {} .--> u )
by FUNCOP_1:72;
defpred S1[ Nat] means (((l1,u) ReassignIn I) -TermEval) | (((S -termsOfMaxDepth) . $1) /\ (SSS *)) = ((((l2,u) ReassignIn I) -TermEval) * (l1 SubstWith l2)) | (((S -termsOfMaxDepth) . $1) /\ (SSS *));
A2:
S1[ 0 ]
proof
reconsider T0 =
(S -termsOfMaxDepth) . 0 as non
empty Subset of
(AllTermsOf S) by FOMODEL1:2;
reconsider T00 =
T0 as non
empty Subset of
((AllSymbolsOf S) *) by XBOOLE_1:1;
reconsider ss =
(l1 SubstWith l2) | ((S -termsOfMaxDepth) . 0) as
(S -termsOfMaxDepth) . 0 -valued Function ;
reconsider X0 =
T0 /\ (SSS *) as
Subset of
T0 ;
reconsider X =
T0 /\ (SSS *) as
Subset of
(AllTermsOf S) by XBOOLE_1:1;
ss | (SSS *) is
T0 -valued
;
then reconsider sss =
(l1 SubstWith l2) | (T0 /\ (SSS *)) as
T00 -valued Function by RELAT_1:71;
A3:
(
dom ((((l2,u) ReassignIn I) -TermEval) * sss) = X &
dom ((((l1,u) ReassignIn I) -TermEval) | X) = X )
by PARTFUN1:def 2;
(
rng ((((l2,u) ReassignIn I) -TermEval) * sss) c= U &
rng ((((l1,u) ReassignIn I) -TermEval) | X) c= U )
by RELAT_1:def 19;
then reconsider f1 =
(((l1,u) ReassignIn I) -TermEval) | X,
f2 =
(((l2,u) ReassignIn I) -TermEval) * sss as
Function of
X,
U by FUNCT_2:2, A3;
now for x being object st x in X holds
f1 . x = f2 . xlet x be
object ;
( x in X implies f1 . b1 = f2 . b1 )assume A4:
x in X
;
f1 . b1 = f2 . b1then reconsider X00 =
X0 as non
empty Subset of
(SSS *) ;
(
dom sss = X &
rng sss c= T0 )
by PARTFUN1:def 2, RELAT_1:def 19;
then reconsider ssss =
sss as
Function of
X00,
T0 by FUNCT_2:2;
reconsider xx =
x as
Element of
X00 by A4;
reconsider xd =
xx as
Element of
SSS * ;
reconsider t0 =
x as
0 -termal string of
S by TARSKI:def 3, FOMODEL1:def 33, A4;
reconsider t00 =
t0 as
Element of
T0 by FOMODEL1:def 33;
T0 = AtomicTermsOf S
by FOMODEL1:def 30;
then reconsider tl =
t00 as 1
-element FinSequence of
LettersOf S by FOMODEL0:12;
reconsider LL =
(LettersOf S) \ {l2} as non
empty Subset of
(LettersOf S) ;
(
rng tl c= LettersOf S &
rng xd c= (AllSymbolsOf S) \ {l2} )
by RELAT_1:def 19;
then
rng xx c= (LettersOf S) /\ ((AllSymbolsOf S) \ {l2})
by XBOOLE_1:19;
then
rng xx c= ((LettersOf S) null (AllSymbolsOf S)) \ {l2}
by XBOOLE_1:49;
then reconsider xxx =
tl as
LL -valued 1
-element FinSequence by RELAT_1:def 19;
{(xxx . 1)} \ LL = {}
;
then reconsider lx =
xxx . 1 as
Element of
LL by ZFMISC_1:60;
not
lx in {l2}
by XBOOLE_0:def 5;
then A5:
(
lx <> l2 & not
lx in dom (l2 .--> ({} .--> u)) )
by TARSKI:def 1;
A6:
len xxx = 1
by CARD_1:def 7;
reconsider newt = (
l1,
l2)
-SymbolSubstIn t0 as
0 -termal string of
S ;
reconsider s1 =
(S -firstChar) . t0,
s2 =
(S -firstChar) . newt as
literal Element of
S ;
A7:
(
s1 = lx &
s2 = newt . 1 )
by FOMODEL0:6;
(
(((((l2,u) ReassignIn I) -TermEval) * ssss) . xx) \+\ ((((l2,u) ReassignIn I) -TermEval) . (ssss . xx)) = {} &
(sss . xx) \+\ ((l1 SubstWith l2) . xx) = {} &
(f1 . xx) \+\ ((((l1,u) ReassignIn I) -TermEval) . xx) = {} )
;
then A8:
(
((((l2,u) ReassignIn I) -TermEval) * sss) . x = (((l2,u) ReassignIn I) -TermEval) . (sss . x) &
sss . x = (l1 SubstWith l2) . x &
f1 . x = (((l1,u) ReassignIn I) -TermEval) . x )
by FOMODEL0:29;
A9:
f2 . x =
(((l2,u) ReassignIn I) -TermEval) . newt
by A8, FOMODEL0:def 22
.=
(((l2,u) ReassignIn I) . s2) . ((((l2,u) ReassignIn I) -TermEval) * (SubTerms newt))
by FOMODEL2:21
.=
(((l2,u) ReassignIn I) . s2) . {}
;
A10:
f1 . x =
(((l1,u) ReassignIn I) . s1) . ((((l1,u) ReassignIn I) -TermEval) * (SubTerms t0))
by A8, FOMODEL2:21
.=
(((l1,u) ReassignIn I) . s1) . {}
;
end;
then
f1 = f2
by FUNCT_2:12;
hence
S1[
0 ]
by RELAT_1:83;
verum
end;
A12:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
reconsider nn =
n,
NN =
n + 1 as
Element of
NAT by ORDINAL1:def 12;
assume A13:
S1[
n]
;
S1[n + 1]
reconsider Tnn =
(S -termsOfMaxDepth) . nn,
TNN =
(S -termsOfMaxDepth) . NN as non
empty Subset of
(AllTermsOf S) by FOMODEL1:2;
reconsider Xn =
Tnn /\ (SSS *),
X =
TNN /\ (SSS *) as
Subset of
(AllTermsOf S) by XBOOLE_1:1;
((l1 SubstWith l2) | ((S -termsOfMaxDepth) . NN)) | (SSS *) is
TNN -valued
;
then reconsider sX =
(l1 SubstWith l2) | X as
AllTermsOf S -valued Function by RELAT_1:71;
(
dom ((l1 SubstWith l2) | X) = X &
rng sX c= AllTermsOf S )
by PARTFUN1:def 2, RELAT_1:def 19;
then reconsider sXX =
sX as
Function of
X,
(AllTermsOf S) by FUNCT_2:2;
((l1 SubstWith l2) | ((S -termsOfMaxDepth) . nn)) | (SSS *) is
Tnn -valued
;
then reconsider sXn =
(l1 SubstWith l2) | Xn as
AllTermsOf S -valued Function by RELAT_1:71;
A14:
(
dom ((((l1,u) ReassignIn I) -TermEval) | X) = X &
dom ((((l2,u) ReassignIn I) -TermEval) * sX) = X &
dom ((((l2,u) ReassignIn I) -TermEval) * sXn) = Xn )
by PARTFUN1:def 2;
(
rng ((((l1,u) ReassignIn I) -TermEval) | X) c= U &
rng ((((l2,u) ReassignIn I) -TermEval) * sX) c= U )
by RELAT_1:def 19;
then reconsider f1 =
(((l1,u) ReassignIn I) -TermEval) | X,
f2 =
(((l2,u) ReassignIn I) -TermEval) * sX as
Function of
X,
U by FUNCT_2:2, A14;
now for x being object st x in X holds
f2 . x = f1 . xlet x be
object ;
( x in X implies f2 . b1 = f1 . b1 )assume A15:
x in X
;
f2 . b1 = f1 . b1then reconsider XX =
X as non
empty Subset of
TNN ;
reconsider xxx =
x as
Element of
XX by A15;
reconsider xx =
xxx as
Element of
SSS * by A15;
reconsider tN =
x as
Element of
TNN by A15;
reconsider t =
tN as
NN -termal string of
S by TARSKI:def 3, FOMODEL1:def 33;
reconsider ttt =
t as
Element of
AllTermsOf S ;
set d =
Depth t;
reconsider aux =
rng xx as
Subset of
((AllSymbolsOf S) \ {l2}) by RELAT_1:def 19;
(
aux * c= SSS * &
rng (SubTerms t) c= (rng t) * )
by RELAT_1:def 19;
then A16:
rng (SubTerms t) c= SSS *
by XBOOLE_1:1;
reconsider tt =
t as
nn + 1
-termal string of
S ;
reconsider newt = (
l1,
l2)
-SymbolSubstIn t as
NN -termal string of
S ;
A17:
rng (SubTerms tt) c= (S -termsOfMaxDepth) . nn
by RELAT_1:def 19;
A18:
(
dom ((((l1,u) ReassignIn I) -TermEval) | Xn) = Xn &
dom (((((l2,u) ReassignIn I) -TermEval) * (l1 SubstWith l2)) | Xn) = Xn )
by A14, RELAT_1:83, PARTFUN1:def 2;
(
(f1 . xxx) \+\ ((((l1,u) ReassignIn I) -TermEval) . xxx) = {} &
(((l1 SubstWith l2) | XX) . xxx) \+\ ((l1 SubstWith l2) . xxx) = {} &
(((((l2,u) ReassignIn I) -TermEval) * sXX) . xxx) \+\ ((((l2,u) ReassignIn I) -TermEval) . (sXX . xxx)) = {} )
;
then A19:
(
f1 . x = (((l1,u) ReassignIn I) -TermEval) . x &
sX . x = (l1 SubstWith l2) . x &
f2 . x = (((l2,u) ReassignIn I) -TermEval) . (sX . x) )
by FOMODEL0:29;
per cases
( Depth t = 0 or Depth t <> 0 )
;
suppose
Depth t = 0
;
f2 . b1 = f1 . b1then reconsider t0 =
t as
0 -termal string of
S by FOMODEL1:def 40;
reconsider l =
(S -firstChar) . t0 as
literal Element of
S ;
A20:
t0 =
<*l*> ^ ((S -multiCat) . (SubTerms t0))
by FOMODEL1:def 37
.=
<*l*> null {}
;
{(xx . 1)} \ SSS = {}
;
then
t0 . 1
in SSS
by ZFMISC_1:60;
then
l in SSS
by FOMODEL0:6;
then
not
l in dom (l2 .--> ({} .--> u))
by XBOOLE_0:def 5;
then A21:
((l2,u) ReassignIn I) . l = I . l
by FUNCT_4:11;
A22:
f1 . t0 =
(((l1,u) ReassignIn I) . l) . ((((l1,u) ReassignIn I) -TermEval) * (SubTerms t0))
by FOMODEL2:21, A19
.=
(((l1,u) ReassignIn I) . l) . {}
;
per cases
( l in dom (l1 .--> ({} .--> u)) or not l in dom (l1 .--> ({} .--> u)) )
;
suppose A23:
l in dom (l1 .--> ({} .--> u))
;
f2 . b1 = f1 . b1
l = l1
by A23, TARSKI:def 1;
then
(
f1 . t0 = (((l1,u) ReassignIn I) . l1) . {} &
(l1 SubstWith l2) . t0 = <*l2*> )
by A22, FOMODEL0:35, A20;
then f2 . t0 =
(((l2,u) ReassignIn I) . ((S -firstChar) . <*l2*>)) . ((((l2,u) ReassignIn I) -TermEval) * (SubTerms <*l2*>))
by FOMODEL2:21, A19
.=
(((l2,u) ReassignIn I) . (<*l2*> . 1)) . {}
by FOMODEL0:6
.=
(((l2,u) ReassignIn I) . l2) . {}
by FINSEQ_1:40
;
hence
f2 . x = f1 . x
by A23, TARSKI:def 1, A22, A1;
verum end; end; suppose
Depth t <> 0
;
f2 . b1 = f1 . b1then A25:
not
t is
0 -termal
;
then reconsider s1 =
(S -firstChar) . t as non
literal ofAtomicFormula Element of
S by FOMODEL1:16;
(
t . 1
= (S -firstChar) . t & not
(S -firstChar) . t is
literal )
by FOMODEL1:16, A25, FOMODEL0:6;
then
newt . 1
= s1
by FUNCT_4:105;
then reconsider s2 =
(S -firstChar) . newt as non
literal ofAtomicFormula Element of
S by FOMODEL0:6;
( not
s1 in dom (l1 .--> ({} .--> u)) & not
s2 in dom (l2 .--> ({} .--> u)) )
by TARSKI:def 1;
then A26:
(
((l1,u) ReassignIn I) . s1 = I . s1 &
((l2,u) ReassignIn I) . s2 = I . s2 )
by FUNCT_4:11;
s1 <> l1
;
then
t . 1
<> l1
by FOMODEL0:6;
then newt . 1 =
t . 1
by FUNCT_4:105
.=
s1
by FOMODEL0:6
;
then A27:
s1 = s2
by FOMODEL0:6;
thus f2 . x =
(((l2,u) ReassignIn I) -TermEval) . newt
by A19, FOMODEL0:def 22
.=
(((l2,u) ReassignIn I) . s2) . ((((l2,u) ReassignIn I) -TermEval) * (SubTerms newt))
by FOMODEL2:21
.=
(((l2,u) ReassignIn I) . s2) . ((((l2,u) ReassignIn I) -TermEval) * ((l1 SubstWith l2) * (SubTerms t)))
by Lm38
.=
(I . s2) . (((((l2,u) ReassignIn I) -TermEval) * (l1 SubstWith l2)) * (SubTerms t))
by A26, RELAT_1:36
.=
(I . s2) . ((((((l2,u) ReassignIn I) -TermEval) * (l1 SubstWith l2)) | (((S -termsOfMaxDepth) . n) /\ (SSS *))) * (SubTerms t))
by RELAT_1:165, A17, A16, XBOOLE_1:19, A18
.=
(I . s2) . ((((l1,u) ReassignIn I) -TermEval) * (SubTerms t))
by RELAT_1:165, A17, A16, XBOOLE_1:19, A18, A13
.=
f1 . x
by A19, A26, A27, FOMODEL2:21
;
verum end; end;
then
f1 = f2
by FUNCT_2:12;
hence
S1[
n + 1]
by RELAT_1:83;
verum
end;
for m being Nat holds S1[m]
from NAT_1:sch 2(A2, A12);
hence
(((l1,u) ReassignIn I) -TermEval) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m)) = ((((l2,u) ReassignIn I) -TermEval) * (l1 SubstWith l2)) | ((((AllSymbolsOf S) \ {l2}) *) /\ ((S -termsOfMaxDepth) . m))
; verum