let X be set ; :: thesis: for S being Language
for U being non empty set
for I1, I2 being b₁,b₂ -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,b₁ -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 Z3: I1 | X = I2 | X ; :: thesis: (I1 -TermEval) | (X *) = (I2 -TermEval) | (X *)
then B2: ( dom (I1 -TermEval) = AllTermsOf S & dom (I2 -TermEval) = AllTermsOf S & I1 | X = I2 | X ) by FUNCT_2:def 1;
defpred S₁[ Nat] means (I1 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . $1)) = (I2 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . $1));
B0: S₁[ 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;
C0: ( dom ((I1 -TermEval) | dd) = (X *) /\ ((S -termsOfMaxDepth) . 0) & dom ((I2 -TermEval) | dd) = (X *) /\ ((S -termsOfMaxDepth) . 0) ) by PARTFUN1:def 2;

now

let x be set ; :: 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 Z0: 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 Z0;
reconsider xd = x as Element of dd by Z0, PARTFUN1:def 2;
reconsider t = x as 0 -termal string of S by Z0, C0, FOMODEL1:def 33;
set o = (S -firstChar) . t;
set ST = SubTerms t;
reconsider XX = X as non empty set by Z0, C0;
reconsider tx = x as non empty Element of XX * by Z0, C0;
{(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 D1: ( (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 Z3, D1
.= ((I2 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . 0))) . x by D1, Th21 ;
:: thesis: verum

end;

hence S₁[ 0 ] by C0, FUNCT_1:2; :: thesis: verum

end;

B1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[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 Z9: S₁[n] ; :: thesis: S₁[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;
C1: ( 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

let x be set ; :: 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 Z4: 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 Z4, C1, FOMODEL1:def 33;
reconsider XX = X as non empty set by Z4, C1;
reconsider DD = DD as non empty Subset of (AllTermsOf S) by Z4;
reconsider tx = x as non empty Element of XX * by Z4, C1;
reconsider dx = x as Element of DD by Z4, PARTFUN1:def 2;
set o = (S -firstChar) . t;
set m = abs (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 Z4, C1, 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 abs (ar ((S -firstChar) . t)) -element FinSequence ;
( ((I1 | X) . oo) \+\ (I1 . oo) = {} & ((I2 | X) . oo) \+\ (I2 . oo) = {} ) ;
then Z10: ( (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 D3: ( ((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 D2: ( ((I1 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . n))) * ST = (I1 -TermEval) * ST & ((I2 -TermEval) | ((X *) /\ ((S -termsOfMaxDepth) . n))) * ST = (I2 -TermEval) * ST ) by C1, RELAT_1:165, XBOOLE_1:19;
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 D3, Z9, Z3, Z10, D2, Th21; :: thesis: verum

end;

hence S₁[n + 1] by C1, FUNCT_1:2; :: thesis: verum

end;

B3: for m being Nat holds S₁[m] from NAT_1:sch 2(B0, B1);
set f1 = (I1 -TermEval) | (X *);
set f2 = (I2 -TermEval) | (X *);
B4: ( dom ((I1 -TermEval) | (X *)) = (X *) /\ (AllTermsOf S) & dom ((I2 -TermEval) | (X *)) = (X *) /\ (AllTermsOf S) ) by B2, RELAT_1:61;

now

let x be set ; :: thesis: ( x in dom ((I1 -TermEval) | (X *)) implies ((I1 -TermEval) | (X *)) . x = ((I2 -TermEval) | (X *)) . x )
assume Z5: 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 Z5, B2, RELAT_1:61;
reconsider t = x as termal string of S by Z5, B4;
set m = Depth t;
reconsider t = t as Depth t -termal string of S by FOMODEL1:def 40;
Z7: ( t in X * & t in (S -termsOfMaxDepth) . (Depth t) ) by Z5, B4, FOMODEL1:def 33;
reconsider Dm = (X *) /\ ((S -termsOfMaxDepth) . (Depth t)) as non empty set by Z7, XBOOLE_0:def 4;
reconsider tt = t as Element of Dm by Z7, XBOOLE_0:def 4;
reconsider xx = x as Element of X * by B4, Z5;
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 B3; :: thesis: verum

end;

hence (I1 -TermEval) | (X *) = (I2 -TermEval) | (X *) by B4, FUNCT_1:2; :: thesis: verum