let X be set ; :: thesis: for S being Language
for l being literal Element of S
for D being RuleSet of S st {(R0 S),(R3a S)} c= D & {(R2 S),(R3b S)} c= D & X is D -expanded holds
X -freeInterpreter l is (X,D) -termEq -respecting
let S be Language; :: thesis: for l being literal Element of S
for D being RuleSet of S st {(R0 S),(R3a S)} c= D & {(R2 S),(R3b S)} c= D & X is D -expanded holds
X -freeInterpreter l is (X,D) -termEq -respecting
let l be literal Element of S; :: thesis: for D being RuleSet of S st {(R0 S),(R3a S)} c= D & {(R2 S),(R3b S)} c= D & X is D -expanded holds
X -freeInterpreter l is (X,D) -termEq -respecting
let D be RuleSet of S; :: thesis: ( {(R0 S),(R3a S)} c= D & {(R2 S),(R3b S)} c= D & X is D -expanded implies X -freeInterpreter l is (X,D) -termEq -respecting )
set AT = AllTermsOf S;
set I = X -freeInterpreter l;
assume ( {(R0 S),(R3a S)} c= D & {(R2 S),(R3b S)} c= D & X is D -expanded ) ; :: thesis: X -freeInterpreter l is (X,D) -termEq -respecting
then reconsider R = (X,D) -termEq as Equivalence_Relation of (AllTermsOf S) by Lm11;
X -freeInterpreter l is R -respecting by Lm50;
hence X -freeInterpreter l is (X,D) -termEq -respecting ; :: thesis: verum