let X be set ; :: thesis: for S being Language
for U being non empty set
for I1, I2 being b1,b2 -interpreter-like Function st I1 | X = I2 | X holds
(I1 -TermEval) | (X *) = (I2 -TermEval) | (X *)
let S be Language; :: thesis: for U being non empty set
for I1, I2 being S,b1 -interpreter-like Function st I1 | X = I2 | X holds
(I1 -TermEval) | (X *) = (I2 -TermEval) | (X *)
let U be non empty set ; :: thesis: for I1, I2 being S,U -interpreter-like Function st I1 | X = I2 | X holds
(I1 -TermEval) | (X *) = (I2 -TermEval) | (X *)
set T = S -termsOfMaxDepth ;
set O = OwnSymbolsOf S;
set TT = AllTermsOf S;
set SS = AllSymbolsOf S;
set L = LettersOf S;
set F = S -firstChar ;
set C = S -multiCat ;
let I1, I2 be S,U -interpreter-like Function; :: thesis: ( I1 | X = I2 | X implies (I1 -TermEval) | (X *) = (I2 -TermEval) | (X *) )
set E1 = I1 -TermEval ;
set E2 = I2 -TermEval ;
set I11 = I1 | X;
set I22 = I2 | X;
assume A1: I1 | X = I2 | X ; :: thesis: (I1 -TermEval) | (X *) = (I2 -TermEval) | (X *)
then A2: ( dom (I1 -TermEval) = AllTermsOf S & dom (I2 -TermEval) = AllTermsOf S & I1 | X = I2 | X ) by FUNCT_2:def 1;
defpred S1[ Nat] means (I1 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . $1)) = (I2 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . $1));
A3: S1[ 0 ]
proof
set d = (X *) /\ ((S -termsOfMaxDepth) . 0);
( (S -termsOfMaxDepth) . 0 c= AllTermsOf S & (X *) /\ ((S -termsOfMaxDepth) . 0) c= (S -termsOfMaxDepth) . 0 ) by FOMODEL1:2;
then reconsider dd = (X *) /\ ((S -termsOfMaxDepth) . 0) as Subset of (AllTermsOf S) by XBOOLE_1:1;
A4: ( dom ((I1 -TermEval) | dd) = (X *) /\ ((S -termsOfMaxDepth) . 0) & dom ((I2 -TermEval) | dd) = (X *) /\ ((S -termsOfMaxDepth) . 0) ) by PARTFUN1:def 2;
now :: thesis: for x being object st x in dom ((I1 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . 0))) holds
((I1 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . 0))) . x = ((I2 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . 0))) . x
let x be object ; :: thesis: ( x in dom ((I1 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . 0))) implies ((I1 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . 0))) . x = ((I2 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . 0))) . x )
assume A5: x in dom ((I1 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . 0))) ; :: thesis: ((I1 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . 0))) . x = ((I2 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . 0))) . x
reconsider dd = dd as non empty Subset of (AllTermsOf S) by A5;
reconsider xd = x as Element of dd by A5;
reconsider t = x as 0 -termal string of S by A5, A4, FOMODEL1:def 33;
set o = (S -firstChar) . t;
set ST = SubTerms t;
reconsider XX = X as non empty set by A5;
reconsider tx = x as non empty Element of XX * by A5, A4;
{(tx . 1)} \ XX = {} ;
then tx . 1 in XX by ZFMISC_1:60;
then reconsider oo = (S -firstChar) . t as Element of XX by FOMODEL0:6;
( ((I1 | X) . oo) \+\ (I1 . oo) = {} & ((I2 | X) . oo) \+\ (I2 . oo) = {} & (((I1 -TermEval) | dd) . xd) \+\ ((I1 -TermEval) . xd) = {} & (((I2 -TermEval) | dd) . xd) \+\ ((I2 -TermEval) . xd) = {} ) ;
then A6: ( (I1 | X) . ((S -firstChar) . t) = I1 . ((S -firstChar) . t) & (I2 | X) . ((S -firstChar) . t) = I2 . ((S -firstChar) . t) & ((I1 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . 0))) . x = (I1 -TermEval) . x & ((I2 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . 0))) . x = (I2 -TermEval) . x ) by FOMODEL0:29;
hence ((I1 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . 0))) . x = (I1 . ((S -firstChar) . t)) . ((I1 -TermEval) * (SubTerms t)) by Th21
.= (I2 . ((S -firstChar) . t)) . ((I2 -TermEval) * (SubTerms t)) by A1, A6
.= ((I2 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . 0))) . x by A6, Th21 ;
:: thesis: verum
end;
hence S1[ 0 ] by A4, FUNCT_1:2; :: thesis: verum
end;
A7: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
set d = (X *) /\ ((S -termsOfMaxDepth) . n);
set D = (X *) /\ ((S -termsOfMaxDepth) . (n + 1));
reconsider nn = n, NN = n + 1 as Element of NAT by ORDINAL1:def 12;
assume A8: S1[n] ; :: thesis: S1[n + 1]
( (X *) /\ ((S -termsOfMaxDepth) . (n + 1)) c= (S -termsOfMaxDepth) . NN & (X *) /\ ((S -termsOfMaxDepth) . n) c= (S -termsOfMaxDepth) . nn & (S -termsOfMaxDepth) . nn c= AllTermsOf S & (S -termsOfMaxDepth) . NN c= AllTermsOf S ) by FOMODEL1:2;
then reconsider DD = (X *) /\ ((S -termsOfMaxDepth) . (n + 1)), dd = (X *) /\ ((S -termsOfMaxDepth) . n) as Subset of (AllTermsOf S) by XBOOLE_1:1;
A9: ( dom ((I1 -TermEval) | dd) = (X *) /\ ((S -termsOfMaxDepth) . n) & dom ((I2 -TermEval) | dd) = (X *) /\ ((S -termsOfMaxDepth) . n) & dom ((I1 -TermEval) | DD) = (X *) /\ ((S -termsOfMaxDepth) . (n + 1)) & dom ((I2 -TermEval) | DD) = (X *) /\ ((S -termsOfMaxDepth) . (n + 1)) ) by PARTFUN1:def 2;
now :: thesis: for x being object st x in dom ((I1 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . (n + 1)))) holds
((I1 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . (n + 1)))) . x = ((I2 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . (n + 1)))) . x
let x be object ; :: thesis: ( x in dom ((I1 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . (n + 1)))) implies ((I1 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . (n + 1)))) . x = ((I2 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . (n + 1)))) . x )
assume A10: x in dom ((I1 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . (n + 1)))) ; :: thesis: ((I1 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . (n + 1)))) . x = ((I2 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . (n + 1)))) . x
reconsider t = x as nn + 1 -termal string of S by A10, A9, FOMODEL1:def 33;
reconsider XX = X as non empty set by A10;
reconsider DD = DD as non empty Subset of (AllTermsOf S) by A10;
reconsider tx = x as non empty Element of XX * by A10, A9;
reconsider dx = x as Element of DD by A10;
set o = (S -firstChar) . t;
set m = |.(ar ((S -firstChar) . t)).|;
{(tx . 1)} \ XX = {} ;
then tx . 1 in XX by ZFMISC_1:60;
then reconsider oo = (S -firstChar) . t as Element of XX by FOMODEL0:6;
reconsider r = rng t as Subset of X by A10, A9, RELAT_1:def 19;
r * c= X * ;
then reconsider newords = (rng t) * as non empty Subset of (X *) ;
reconsider ST = SubTerms t as newords -valued |.(ar ((S -firstChar) . t)).| -element FinSequence ;
( ((I1 | X) . oo) \+\ (I1 . oo) = {} & ((I2 | X) . oo) \+\ (I2 . oo) = {} ) ;
then A11: ( (I1 | X) . oo = I1 . oo & (I2 | X) . oo = I2 . oo ) by FOMODEL0:29;
( (((I1 -TermEval) | DD) . dx) \+\ ((I1 -TermEval) . dx) = {} & (((I2 -TermEval) | DD) . dx) \+\ ((I2 -TermEval) . dx) = {} ) ;
then A12: ( ((I1 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . (n + 1)))) . x = (I1 -TermEval) . x & ((I2 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . (n + 1)))) . x = (I2 -TermEval) . x ) by FOMODEL0:29;
( rng ST c= (S -termsOfMaxDepth) . nn & rng ST c= X * ) by RELAT_1:def 19;
then A13: ( ((I1 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . n))) * ST = (I1 -TermEval) * ST & ((I2 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . n))) * ST = (I2 -TermEval) * ST ) by XBOOLE_1:19, A9, RELAT_1:165;
then (I1 . ((S -firstChar) . t)) . (((I1 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . n))) * ST) = (I1 -TermEval) . t by Th21;
hence ((I1 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . (n + 1)))) . x = ((I2 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . (n + 1)))) . x by A12, A8, A1, A11, A13, Th21; :: thesis: verum
end;
hence S1[n + 1] by A9, FUNCT_1:2; :: thesis: verum
end;
A14: for m being Nat holds S1[m] from NAT_1:sch 2(A3, A7);
 set f1 = (I1 -TermEval) | (X *);
set f2 = (I2 -TermEval) | (X *);
A15: ( dom ((I1 -TermEval) | (X *)) = (X *) /\ (AllTermsOf S) & dom ((I2 -TermEval) | (X *)) = (X *) /\ (AllTermsOf S) ) by RELAT_1:61, A2;
now :: thesis: for x being object st x in dom ((I1 -TermEval) | (X *)) holds
((I1 -TermEval) | (X *)) . x = ((I2 -TermEval) | (X *)) . x
let x be object ; :: thesis: ( x in dom ((I1 -TermEval) | (X *)) implies ((I1 -TermEval) | (X *)) . x = ((I2 -TermEval) | (X *)) . x )
assume A16: x in dom ((I1 -TermEval) | (X *)) ; :: thesis: ((I1 -TermEval) | (X *)) . x = ((I2 -TermEval) | (X *)) . x
reconsider D = (X *) /\ (AllTermsOf S) as non empty Subset of (AllTermsOf S) by A16, RELAT_1:61, A2;
reconsider t = x as termal string of S by A16, A15;
set m = Depth t;
reconsider t = t as Depth t -termal string of S by FOMODEL1:def 40;
A17: ( t in X * & t in (S -termsOfMaxDepth) . (Depth t) ) by A16, FOMODEL1:def 33;
reconsider Dm = (X *) /\ ((S -termsOfMaxDepth) . (Depth t)) as non empty set by A17, XBOOLE_0:def 4;
reconsider tt = t as Element of Dm by A17, XBOOLE_0:def 4;
reconsider xx = x as Element of X * by A16;
set g1 = (I1 -TermEval) | Dm;
set g2 = (I2 -TermEval) | Dm;
( (((I1 -TermEval) | (X *)) . xx) \+\ ((I1 -TermEval) . xx) = {} & (((I2 -TermEval) | (X *)) . xx) \+\ ((I2 -TermEval) . xx) = {} & (((I1 -TermEval) | Dm) . tt) \+\ ((I1 -TermEval) . tt) = {} & (((I2 -TermEval) | Dm) . tt) \+\ ((I2 -TermEval) . tt) = {} ) ;
then ( ((I1 -TermEval) | (X *)) . x = (I1 -TermEval) . x & ((I2 -TermEval) | (X *)) . x = (I2 -TermEval) . x & ((I1 -TermEval) | Dm) . x = (I1 -TermEval) . x & ((I2 -TermEval) | Dm) . x = (I2 -TermEval) . x ) by FOMODEL0:29;
hence ((I1 -TermEval) | (X *)) . x = ((I2 -TermEval) | (X *)) . x by A14; :: thesis: verum
end;
hence (I1 -TermEval) | (X *) = (I2 -TermEval) | (X *) by A15, FUNCT_1:2; :: thesis: verum