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

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