:: Regular Expression Quantifiers -- at least $m$ Occurrences
:: by Micha{\l} Trybulec
::
:: Received October 9, 2007
:: Copyright (c) 2007 Association of Mizar Users
theorem :: FLANG_3:1
:: deftheorem defines |^.. FLANG_3:def 1 :
theorem Th2: :: FLANG_3:2
theorem Th3: :: FLANG_3:3
theorem Th4: :: FLANG_3:4
theorem Th5: :: FLANG_3:5
theorem Th6: :: FLANG_3:6
theorem Th7: :: FLANG_3:7
theorem :: FLANG_3:8
theorem Th9: :: FLANG_3:9
theorem Th10: :: FLANG_3:10
theorem Th11: :: FLANG_3:11
theorem :: FLANG_3:12
theorem Th13: :: FLANG_3:13
theorem Th14: :: FLANG_3:14
theorem Th15: :: FLANG_3:15
theorem Th16: :: FLANG_3:16
theorem Th17: :: FLANG_3:17
theorem Th18: :: FLANG_3:18
theorem Th19: :: FLANG_3:19
theorem :: FLANG_3:20
theorem Th21: :: FLANG_3:21
theorem Th22: :: FLANG_3:22
theorem Th23: :: FLANG_3:23
theorem Th24: :: FLANG_3:24
theorem Th25: :: FLANG_3:25
theorem :: FLANG_3:26
theorem Th27: :: FLANG_3:27
theorem Th28: :: FLANG_3:28
theorem Th29: :: FLANG_3:29
theorem Th30: :: FLANG_3:30
theorem :: FLANG_3:31
theorem Th32: :: FLANG_3:32
theorem Th33: :: FLANG_3:33
theorem :: FLANG_3:34
theorem Th35: :: FLANG_3:35
theorem :: FLANG_3:36
theorem Th37: :: FLANG_3:37
theorem Th38: :: FLANG_3:38
theorem :: FLANG_3:39
theorem Th40: :: FLANG_3:40
theorem Th41: :: FLANG_3:41
theorem :: FLANG_3:42
theorem :: FLANG_3:43
theorem Th44: :: FLANG_3:44
theorem Th45: :: FLANG_3:45
theorem Th46: :: FLANG_3:46
theorem Th47: :: FLANG_3:47
:: deftheorem defines + FLANG_3:def 2 :
theorem Th48: :: FLANG_3:48
theorem Th49: :: FLANG_3:49
theorem Th50: :: FLANG_3:50
theorem :: FLANG_3:51
theorem Th52: :: FLANG_3:52
theorem Th53: :: FLANG_3:53
theorem :: FLANG_3:54
theorem Th55: :: FLANG_3:55
theorem Th56: :: FLANG_3:56
theorem Th57: :: FLANG_3:57
theorem Th58: :: FLANG_3:58
theorem Th59: :: FLANG_3:59
theorem Th60: :: FLANG_3:60
theorem Th61: :: FLANG_3:61
theorem :: FLANG_3:62
theorem :: FLANG_3:63
theorem :: FLANG_3:64
theorem :: FLANG_3:65
theorem Th66: :: FLANG_3:66
theorem :: FLANG_3:67
theorem :: FLANG_3:68
theorem :: FLANG_3:69
theorem :: FLANG_3:70
theorem :: FLANG_3:71
theorem Th72: :: FLANG_3:72
theorem :: FLANG_3:73
theorem :: FLANG_3:74
theorem Th75: :: FLANG_3:75
theorem :: FLANG_3:76
theorem :: FLANG_3:77
theorem :: FLANG_3:78
theorem :: FLANG_3:79
theorem :: FLANG_3:80
theorem :: FLANG_3:81
theorem :: FLANG_3:82
theorem :: FLANG_3:83
theorem :: FLANG_3:84
theorem :: FLANG_3:85
theorem Th86: :: FLANG_3:86
theorem Th87: :: FLANG_3:87
theorem :: FLANG_3:88
theorem :: FLANG_3:89
theorem Th90: :: FLANG_3:90
theorem :: FLANG_3:91
theorem Th92: :: FLANG_3:92
theorem :: FLANG_3:93
theorem :: FLANG_3:94
theorem :: FLANG_3:95
theorem :: FLANG_3:96