let X be set ; for S being Language
for D being RuleSet of S st {(R#3a S)} c= D & X is D -expanded holds
(X,D) -termEq is transitive
let S be Language; for D being RuleSet of S st {(R#3a S)} c= D & X is D -expanded holds
(X,D) -termEq is transitive
let D be RuleSet of S; ( {(R#3a S)} c= D & X is D -expanded implies (X,D) -termEq is transitive )
set AT = AllTermsOf S;
set E = TheEqSymbOf S;
set Q = S -sequents ;
set AF = AllFormulasOf S;
set E3 = R#3a S;
set R = (X,D) -termEq ;
set G3 = {(R#3a S)};
assume A1:
{(R#3a S)} c= D
; ( not X is D -expanded or (X,D) -termEq is transitive )
then reconsider DD = D as non empty RuleSet of S ;
reconsider GG3 = {(R#3a S)} as non empty Subset of DD by A1;
assume A2:
X is D -expanded
; (X,D) -termEq is transitive
A3:
field ((X,D) -termEq) c= (AllTermsOf S) \/ (AllTermsOf S)
by RELSET_1:8;
now for x, y, z being object st x in field ((X,D) -termEq) & y in field ((X,D) -termEq) & z in field ((X,D) -termEq) & [x,y] in (X,D) -termEq & [y,z] in (X,D) -termEq holds
[x,z] in (X,D) -termEq let x,
y,
z be
object ;
( x in field ((X,D) -termEq) & y in field ((X,D) -termEq) & z in field ((X,D) -termEq) & [x,y] in (X,D) -termEq & [y,z] in (X,D) -termEq implies [x,z] in (X,D) -termEq )assume
(
x in field ((X,D) -termEq) &
y in field ((X,D) -termEq) &
z in field ((X,D) -termEq) )
;
( [x,y] in (X,D) -termEq & [y,z] in (X,D) -termEq implies [x,z] in (X,D) -termEq )then reconsider tt1 =
x,
tt2 =
y,
tt3 =
z as
Element of
AllTermsOf S by A3;
reconsider t1 =
tt1,
t2 =
tt2,
t3 =
tt3 as
termal string of
S ;
set phi1 =
(<*(TheEqSymbOf S)*> ^ t1) ^ t2;
set phi2 =
(<*(TheEqSymbOf S)*> ^ t2) ^ t3;
set phi3 =
(<*(TheEqSymbOf S)*> ^ t1) ^ t3;
assume
(
[x,y] in (
X,
D)
-termEq &
[y,z] in (
X,
D)
-termEq )
;
[x,z] in (X,D) -termEq then A4:
(
(<*(TheEqSymbOf S)*> ^ t1) ^ t2 is
X,
D -provable &
(<*(TheEqSymbOf S)*> ^ t2) ^ t3 is
X,
D -provable )
by Lm23;
reconsider XX =
X as non
empty set by A2, A4;
reconsider phi11 =
(<*(TheEqSymbOf S)*> ^ t1) ^ t2,
phi22 =
(<*(TheEqSymbOf S)*> ^ t2) ^ t3 as
Element of
XX by A4, A2;
reconsider Phi =
{phi11,phi22} as non
empty Subset of
XX ;
[{((<*(TheEqSymbOf S)*> ^ t1) ^ t2),((<*(TheEqSymbOf S)*> ^ t2) ^ t3)},((<*(TheEqSymbOf S)*> ^ t1) ^ t3)] is 1,
{} ,
{(R#3a S)} -derivable
;
then
(
[Phi,((<*(TheEqSymbOf S)*> ^ t1) ^ t3)] is 1,
{} ,
{(R#3a S)} -derivable &
GG3 c= D )
;
then
[Phi,((<*(TheEqSymbOf S)*> ^ t1) ^ t3)] is 1,
{} ,
DD -derivable
by Th2;
then
(<*(TheEqSymbOf S)*> ^ t1) ^ t3 is
X,
DD -provable
;
hence
[x,z] in (
X,
D)
-termEq
;
verum end;
hence
(X,D) -termEq is transitive
by RELAT_2:def 8, RELAT_2:def 16; verum