let X be set ; for S being Language
for D being RuleSet of S
for s being low-compounding Element of S st {(R#3d S)} c= D & X is D -expanded & s is termal holds
X -freeInterpreter s is (X,D) -termEq -respecting
let S be Language; for D being RuleSet of S
for s being low-compounding Element of S st {(R#3d S)} c= D & X is D -expanded & s is termal holds
X -freeInterpreter s is (X,D) -termEq -respecting
let D be RuleSet of S; for s being low-compounding Element of S st {(R#3d S)} c= D & X is D -expanded & s is termal holds
X -freeInterpreter s is (X,D) -termEq -respecting
let s be low-compounding Element of S; ( {(R#3d S)} c= D & X is D -expanded & s is termal implies X -freeInterpreter s is (X,D) -termEq -respecting )
set n = |.(ar s).|;
set AT = AllTermsOf S;
set E = TheEqSymbOf S;
set Phi = X;
set R = (X,D) -termEq ;
set I = X -freeInterpreter s;
assume A1:
{(R#3d S)} c= D
; ( not X is D -expanded or not s is termal or X -freeInterpreter s is (X,D) -termEq -respecting )
assume A2:
X is D -expanded
; ( not s is termal or X -freeInterpreter s is (X,D) -termEq -respecting )
assume
s is termal
; X -freeInterpreter s is (X,D) -termEq -respecting
then reconsider ss = s as termal Element of S ;
A3:
not ss is relational
;
now for x1, x2 being set st [x1,x2] in |.(ar s).| -placesOf ((X,D) -termEq) holds
[((X -freeInterpreter s) . x1),((X -freeInterpreter s) . x2)] in (X,D) -termEq let x1,
x2 be
set ;
( [x1,x2] in |.(ar s).| -placesOf ((X,D) -termEq) implies [((X -freeInterpreter s) . x1),((X -freeInterpreter s) . x2)] in (X,D) -termEq )assume
[x1,x2] in |.(ar s).| -placesOf ((X,D) -termEq)
;
[((X -freeInterpreter s) . x1),((X -freeInterpreter s) . x2)] in (X,D) -termEq then consider T1,
T2 being
|.(ar s).| -element Element of
(AllTermsOf S) * such that A4:
(
T1 = x1 &
T2 = x2 &
PairWiseEq (
T1,
T2)
c= X )
by Lm37, A2;
set Z =
PairWiseEq (
T1,
T2);
reconsider t1 =
ss -compound T1,
t2 =
ss -compound T2 as
termal string of
S ;
reconsider ZZ =
PairWiseEq (
T1,
T2) as
Subset of
X by A4;
{[(PairWiseEq (T1,T2)),((<*(TheEqSymbOf S)*> ^ t1) ^ t2)]} is
{} ,
{(R#3d S)} -derivable
by Lm35;
then A5:
{[(PairWiseEq (T1,T2)),((<*(TheEqSymbOf S)*> ^ t1) ^ t2)]} is
{} ,
D -derivable
by A1, Lm18;
A6:
(<*(TheEqSymbOf S)*> ^ t1) ^ t2 is
ZZ,
D -provable
by A5;
(
(X -freeInterpreter s) . T1 = t1 &
(X -freeInterpreter s) . T2 = t2 )
by FOMODEL3:6;
hence
[((X -freeInterpreter s) . x1),((X -freeInterpreter s) . x2)] in (
X,
D)
-termEq
by A6, A4;
verum end;
then
X -freeInterpreter s is |.(ar s).| -placesOf ((X,D) -termEq),(X,D) -termEq -respecting
;
hence
X -freeInterpreter s is (X,D) -termEq -respecting
by FOMODEL3:def 10, A3; verum