let X be set ; :: thesis: for S being Language
for t1, t2 being termal string of S
for D being RuleSet of S holds
( [t1,t2] in (X,D) -termEq iff (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is X,D -provable )
let S be Language; :: thesis: for t1, t2 being termal string of S
for D being RuleSet of S holds
( [t1,t2] in (X,D) -termEq iff (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is X,D -provable )
let t1, t2 be termal string of S; :: thesis: for D being RuleSet of S holds
( [t1,t2] in (X,D) -termEq iff (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is X,D -provable )
let D be RuleSet of S; :: thesis: ( [t1,t2] in (X,D) -termEq iff (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is X,D -provable )
set E = TheEqSymbOf S;
set R = (X,D) -termEq ;
thus ( [t1,t2] in (X,D) -termEq implies (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is X,D -provable ) :: thesis: ( (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is X,D -provable implies [t1,t2] in (X,D) -termEq )
proof
assume [t1,t2] in (X,D) -termEq ; :: thesis: (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is X,D -provable
then consider t11, t22 being termal string of S such that
A1: ( [t11,t22] = [t1,t2] & (<*(TheEqSymbOf S)*> ^ t11) ^ t22 is X,D -provable ) ;
( t11 = t1 & t22 = t2 & (<*(TheEqSymbOf S)*> ^ t11) ^ t22 is X,D -provable ) by A1, XTUPLE_0:1;
hence (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is X,D -provable ; :: thesis: verum
end;
assume (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is X,D -provable ; :: thesis: [t1,t2] in (X,D) -termEq
hence [t1,t2] in (X,D) -termEq ; :: thesis: verum