let X be set ; :: thesis: for S being Language
for a being ofAtomicFormula Element of S
for D being RuleSet of S st {(R#3a S)} c= D & D /\ {(R#3d S)} = {(R#3d S)} & {(R#2 S)} /\ D = {(R#2 S)} & {(R#3b S)} /\ D = {(R#3b S)} & D /\ {(R#3e S)} = {(R#3e S)} & X is D -expanded holds
X -freeInterpreter a is (X,D) -termEq -respecting
let S be Language; :: thesis: for a being ofAtomicFormula Element of S
for D being RuleSet of S st {(R#3a S)} c= D & D /\ {(R#3d S)} = {(R#3d S)} & {(R#2 S)} /\ D = {(R#2 S)} & {(R#3b S)} /\ D = {(R#3b S)} & D /\ {(R#3e S)} = {(R#3e S)} & X is D -expanded holds
X -freeInterpreter a is (X,D) -termEq -respecting
let a be ofAtomicFormula Element of S; :: thesis: for D being RuleSet of S st {(R#3a S)} c= D & D /\ {(R#3d S)} = {(R#3d S)} & {(R#2 S)} /\ D = {(R#2 S)} & {(R#3b S)} /\ D = {(R#3b S)} & D /\ {(R#3e S)} = {(R#3e S)} & X is D -expanded holds
X -freeInterpreter a is (X,D) -termEq -respecting
let D be RuleSet of S; :: thesis: ( {(R#3a S)} c= D & D /\ {(R#3d S)} = {(R#3d S)} & {(R#2 S)} /\ D = {(R#2 S)} & {(R#3b S)} /\ D = {(R#3b S)} & D /\ {(R#3e S)} = {(R#3e S)} & X is D -expanded implies X -freeInterpreter a is (X,D) -termEq -respecting )
set s = a;
set AT = AllTermsOf S;
set I = X -freeInterpreter a;
set AF = AtomicFormulasOf S;
set ch = chi (X,(AtomicFormulasOf S));
set SS = AllSymbolsOf S;
set n = |.(ar a).|;
set f = a -compound ;
set R = (X,D) -termEq ;
assume A1: ( {(R#3a S)} c= D & D /\ {(R#3d S)} = {(R#3d S)} & {(R#2 S)} /\ D = {(R#2 S)} & {(R#3b S)} /\ D = {(R#3b S)} & D /\ {(R#3e S)} = {(R#3e S)} & X is D -expanded ) ; :: thesis: X -freeInterpreter a is (X,D) -termEq -respecting
then reconsider S2 = {(R#2 S)}, S3 = {(R#3b S)} as Subset of D ;
A2: S2 \/ S3 c= D ;