let X be set ; :: thesis: for S being Language
for D being RuleSet of S st {(R#2 S)} c= D holds
(X,D) -termEq is total
let S be Language; :: thesis: for D being RuleSet of S st {(R#2 S)} c= D holds
(X,D) -termEq is total
let D be RuleSet of S; :: thesis: ( {(R#2 S)} c= D implies (X,D) -termEq is total )
assume A1: {(R#2 S)} c= D ; :: thesis: (X,D) -termEq is total
set AT = AllTermsOf S;
set E = TheEqSymbOf S;
set Phi = X;
set R = (X,D) -termEq ;
now :: thesis: for x being object st x in AllTermsOf S holds
x in dom ((X,D) -termEq)
let x be object ; :: thesis: ( x in AllTermsOf S implies x in dom ((X,D) -termEq) )
assume x in AllTermsOf S ; :: thesis: x in dom ((X,D) -termEq)
then reconsider t = x as termal string of S ;
set phi = (<*(TheEqSymbOf S)*> ^ t) ^ t;
set seqt = [{},((<*(TheEqSymbOf S)*> ^ t) ^ t)];
{[{},((<*(TheEqSymbOf S)*> ^ t) ^ t)]} is {} ,D -derivable by A1, Lm18;
then (<*(TheEqSymbOf S)*> ^ t) ^ t is {} \ (X \ {}),D -provable ;
then (<*(TheEqSymbOf S)*> ^ t) ^ t is X \/ {},D -provable ;
then [t,t] in (X,D) -termEq ;
hence x in dom ((X,D) -termEq) by XTUPLE_0:def 12; :: thesis: verum
end;
then AllTermsOf S c= dom ((X,D) -termEq) by TARSKI:def 3;
hence (X,D) -termEq is total by PARTFUN1:def 2, XBOOLE_0:def 10; :: thesis: verum