let X be set ; for S being Language
for D being RuleSet of S st {(R#3b S)} c= D & X is D -expanded holds
(X,D) -termEq is symmetric
let S be Language; for D being RuleSet of S st {(R#3b S)} c= D & X is D -expanded holds
(X,D) -termEq is symmetric
let D be RuleSet of S; ( {(R#3b S)} c= D & X is D -expanded implies (X,D) -termEq is symmetric )
set AT = AllTermsOf S;
set E = TheEqSymbOf S;
set Q = S -sequents ;
set AF = AllFormulasOf S;
set Phi = X;
set R = (X,D) -termEq ;
assume A1:
{(R#3b S)} c= D
; ( not X is D -expanded or (X,D) -termEq is symmetric )
assume A2:
X is D -expanded
; (X,D) -termEq is symmetric
A3:
field ((X,D) -termEq) c= (AllTermsOf S) \/ (AllTermsOf S)
by RELSET_1:8;
now for x, y being object st x in field ((X,D) -termEq) & y in field ((X,D) -termEq) & [x,y] in (X,D) -termEq holds
[y,x] in (X,D) -termEq let x,
y be
object ;
( x in field ((X,D) -termEq) & y in field ((X,D) -termEq) & [x,y] in (X,D) -termEq implies [y,x] in (X,D) -termEq )assume
(
x in field ((X,D) -termEq) &
y in field ((X,D) -termEq) )
;
( [x,y] in (X,D) -termEq implies [y,x] in (X,D) -termEq )then reconsider tt1 =
x,
tt2 =
y as
Element of
AllTermsOf S by A3;
reconsider t1 =
tt1,
t2 =
tt2 as
termal string of
S ;
reconsider phi1 =
(<*(TheEqSymbOf S)*> ^ t1) ^ t2 as
wff string of
S ;
reconsider phi2 =
(<*(TheEqSymbOf S)*> ^ t2) ^ t1 as
wff string of
S ;
reconsider seqt =
[{phi1},phi2] as
Element of
S -sequents by Def2;
reconsider Seqts =
{} as
Element of
bool (S -sequents) by XBOOLE_1:2;
A5:
seqt Rule3b {}
;
[Seqts,seqt] in P#3b S
by A5, Def38;
then
seqt in (R#3b S) . Seqts
by Lm27;
then
{seqt} is
{} ,
{(R#3b S)} -derivable
by Lm20, ZFMISC_1:31;
then
{seqt} is
{} ,
D -derivable
by A1, Lm18;
then A6:
phi2 is
{phi1},
D -provable
;
assume
[x,y] in (
X,
D)
-termEq
;
[y,x] in (X,D) -termEq then consider t11,
t22 being
termal string of
S such that A7:
(
[x,y] = [t11,t22] &
(<*(TheEqSymbOf S)*> ^ t11) ^ t22 is
X,
D -provable )
;
(
t1 = t11 &
t2 = t22 )
by XTUPLE_0:1, A7;
then
{phi1} c= X
by A2, A7;
hence
[y,x] in (
X,
D)
-termEq
by A6;
verum end;
hence
(X,D) -termEq is symmetric
by RELAT_2:def 3, RELAT_2:def 11; verum