let E be set ; for S being semi-Thue-system of E
for s, t, u, v being Element of E ^omega st s ==>* t,S & u ==>. v,{[s,t]} holds
u ==>* v,S
let S be semi-Thue-system of E; for s, t, u, v being Element of E ^omega st s ==>* t,S & u ==>. v,{[s,t]} holds
u ==>* v,S
let s, t, u, v be Element of E ^omega ; ( s ==>* t,S & u ==>. v,{[s,t]} implies u ==>* v,S )
assume that
A1:
s ==>* t,S
and
A2:
u ==>. v,{[s,t]}
; u ==>* v,S
consider u1, v1, s1, t1 being Element of E ^omega such that
A3:
( u = (u1 ^ s1) ^ v1 & v = (u1 ^ t1) ^ v1 )
and
A4:
s1 -->. t1,{[s,t]}
by A2;
[s1,t1] in {[s,t]}
by A4;
then
[s1,t1] = [s,t]
by TARSKI:def 1;
then
( s1 = s & t1 = t )
by XTUPLE_0:1;
hence
u ==>* v,S
by A1, A3, Th37; verum