let E be set ; :: thesis: 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; :: thesis: 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 ; :: thesis: ( s ==>* t,S & u ==>. v,{[s,t]} implies u ==>* v,S )
assume that
A1: s ==>* t,S and
A2: u ==>. v,{[s,t]} ; :: thesis: 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; :: thesis: verum