:: String Rewriting Systems
:: by Micha{\l} Trybulec
::
:: Received July 17, 2007
:: Copyright (c) 2007 Association of Mizar Users
theorem Th1: :: REWRITE2:1
theorem Th2: :: REWRITE2:2
theorem Th3: :: REWRITE2:3
theorem Th4: :: REWRITE2:4
:: deftheorem Def1 defines XFinSequence-yielding REWRITE2:def 1 :
:: deftheorem Def2 defines ^+ REWRITE2:def 2 :
:: deftheorem Def3 defines +^ REWRITE2:def 3 :
theorem Th5: :: REWRITE2:5
theorem :: REWRITE2:6
theorem :: REWRITE2:7
theorem :: REWRITE2:8
theorem :: REWRITE2:9
:: deftheorem Def4 defines -->. REWRITE2:def 4 :
:: deftheorem Def5 defines ==>. REWRITE2:def 5 :
theorem Th10: :: REWRITE2:10
theorem :: REWRITE2:11
theorem Th12: :: REWRITE2:12
theorem Th13: :: REWRITE2:13
theorem Th14: :: REWRITE2:14
theorem Th15: :: REWRITE2:15
theorem Th16: :: REWRITE2:16
theorem Th17: :: REWRITE2:17
theorem Th18: :: REWRITE2:18
theorem Th19: :: REWRITE2:19
theorem Th20: :: REWRITE2:20
theorem Th21: :: REWRITE2:21
definition
let E be
set ;
let S be
semi-Thue-system of
E;
func ==>.-relation S -> Relation of
E ^omega means :
Def6:
:: REWRITE2:def 6
for
s,
t being
Element of
E ^omega holds
(
[s,t] in it iff
s ==>. t,
S );
existence
ex b1 being Relation of E ^omega st
for s, t being Element of E ^omega holds
( [s,t] in b1 iff s ==>. t,S )
uniqueness
for b1, b2 being Relation of E ^omega st ( for s, t being Element of E ^omega holds
( [s,t] in b1 iff s ==>. t,S ) ) & ( for s, t being Element of E ^omega holds
( [s,t] in b2 iff s ==>. t,S ) ) holds
b1 = b2
end;
:: deftheorem Def6 defines ==>.-relation REWRITE2:def 6 :
theorem Th22: :: REWRITE2:22
theorem Th23: :: REWRITE2:23
theorem :: REWRITE2:24
theorem Th25: :: REWRITE2:25
theorem Th26: :: REWRITE2:26
theorem Th27: :: REWRITE2:27
theorem Th28: :: REWRITE2:28
theorem Th29: :: REWRITE2:29
theorem Th30: :: REWRITE2:30
theorem Th31: :: REWRITE2:31
:: deftheorem Def7 defines ==>* REWRITE2:def 7 :
theorem Th32: :: REWRITE2:32
theorem Th33: :: REWRITE2:33
theorem :: REWRITE2:34
theorem Th35: :: REWRITE2:35
theorem Th36: :: REWRITE2:36
theorem Th37: :: REWRITE2:37
theorem :: REWRITE2:38
theorem :: REWRITE2:39
theorem Th40: :: REWRITE2:40
theorem Th41: :: REWRITE2:41
theorem Th42: :: REWRITE2:42
theorem Th43: :: REWRITE2:43
theorem Th44: :: REWRITE2:44
theorem Th45: :: REWRITE2:45
:: deftheorem defines Lang REWRITE2:def 8 :
theorem Th46: :: REWRITE2:46
theorem Th47: :: REWRITE2:47
theorem Th48: :: REWRITE2:48
theorem Th49: :: REWRITE2:49
theorem Th50: :: REWRITE2:50
theorem :: REWRITE2:51
:: deftheorem Def9 defines are_equivalent_wrt REWRITE2:def 9 :
theorem :: REWRITE2:52
theorem :: REWRITE2:53
theorem :: REWRITE2:54
theorem :: REWRITE2:55
theorem Th56: :: REWRITE2:56
theorem Th57: :: REWRITE2:57
theorem Th58: :: REWRITE2:58
theorem Th59: :: REWRITE2:59
theorem Th60: :: REWRITE2:60
theorem :: REWRITE2:61
theorem :: REWRITE2:62