:: Regular Expression Quantifiers -- $m$ to $n$ Occurrences
:: by Micha{\l} Trybulec
::
:: Received June 6, 2007
:: Copyright (c) 2007 Association of Mizar Users
theorem Th1: :: FLANG_2:1
for
m,
k,
i,
n being
Nat st
m + k <= i &
i <= n + k holds
ex
mn being
Nat st
(
mn + k = i &
m <= mn &
mn <= n )
theorem Th2: :: FLANG_2:2
for
m,
n,
k,
l,
i being
Nat st
m <= n &
k <= l &
m + k <= i &
i <= n + l holds
ex
mn,
kl being
Nat st
(
mn + kl = i &
m <= mn &
mn <= n &
k <= kl &
kl <= l )
theorem Th3: :: FLANG_2:3
for
m,
n being
Nat st
m < n holds
ex
k being
Nat st
(
m + k = n &
k > 0 )
theorem Th4: :: FLANG_2:4
theorem :: FLANG_2:5
theorem :: FLANG_2:6
theorem Th7: :: FLANG_2:7
theorem :: FLANG_2:8
theorem Th9: :: FLANG_2:9
theorem Th10: :: FLANG_2:10
theorem :: FLANG_2:11
theorem Th12: :: FLANG_2:12
theorem :: FLANG_2:13
theorem :: FLANG_2:14
theorem :: FLANG_2:15
theorem Th16: :: FLANG_2:16
theorem Th17: :: FLANG_2:17
theorem :: FLANG_2:18
:: deftheorem defines |^ FLANG_2:def 1 :
theorem Th19: :: FLANG_2:19
theorem Th20: :: FLANG_2:20
theorem Th21: :: FLANG_2:21
theorem Th22: :: FLANG_2:22
theorem Th23: :: FLANG_2:23
theorem :: FLANG_2:24
theorem Th25: :: FLANG_2:25
theorem Th26: :: FLANG_2:26
theorem :: FLANG_2:27
theorem Th28: :: FLANG_2:28
theorem Th29: :: FLANG_2:29
theorem Th30: :: FLANG_2:30
theorem Th31: :: FLANG_2:31
theorem Th32: :: FLANG_2:32
theorem Th33: :: FLANG_2:33
theorem Th34: :: FLANG_2:34
theorem Th35: :: FLANG_2:35
theorem Th36: :: FLANG_2:36
theorem Th37: :: FLANG_2:37
theorem Th38: :: FLANG_2:38
theorem Th39: :: FLANG_2:39
theorem Th40: :: FLANG_2:40
theorem Th41: :: FLANG_2:41
theorem Th42: :: FLANG_2:42
theorem :: FLANG_2:43
theorem :: FLANG_2:44
theorem Th45: :: FLANG_2:45
theorem Th46: :: FLANG_2:46
theorem :: FLANG_2:47
theorem :: FLANG_2:48
theorem :: FLANG_2:49
theorem :: FLANG_2:50
theorem Th51: :: FLANG_2:51
theorem Th52: :: FLANG_2:52
theorem Th53: :: FLANG_2:53
theorem :: FLANG_2:54
theorem :: FLANG_2:55
theorem :: FLANG_2:56
theorem :: FLANG_2:57
theorem :: FLANG_2:58
theorem :: FLANG_2:59
theorem :: FLANG_2:60
theorem :: FLANG_2:61
theorem :: FLANG_2:62
theorem :: FLANG_2:63
theorem Th64: :: FLANG_2:64
theorem :: FLANG_2:65
theorem Th66: :: FLANG_2:66
theorem :: FLANG_2:67
theorem :: FLANG_2:68
theorem Th69: :: FLANG_2:69
theorem :: FLANG_2:70
theorem Th71: :: FLANG_2:71
theorem Th72: :: FLANG_2:72
:: deftheorem defines ? FLANG_2:def 2 :
theorem Th73: :: FLANG_2:73
theorem :: FLANG_2:74
theorem Th75: :: FLANG_2:75
theorem Th76: :: FLANG_2:76
theorem :: FLANG_2:77
theorem Th78: :: FLANG_2:78
theorem Th79: :: FLANG_2:79
theorem Th80: :: FLANG_2:80
theorem :: FLANG_2:81
theorem :: FLANG_2:82
theorem :: FLANG_2:83
theorem :: FLANG_2:84
theorem :: FLANG_2:85
theorem :: FLANG_2:86
theorem :: FLANG_2:87
theorem :: FLANG_2:88
theorem :: FLANG_2:89
theorem :: FLANG_2:90
theorem :: FLANG_2:91
theorem :: FLANG_2:92
theorem Th93: :: FLANG_2:93
theorem Th94: :: FLANG_2:94
theorem Th95: :: FLANG_2:95
theorem Th96: :: FLANG_2:96
theorem Th97: :: FLANG_2:97
theorem Th98: :: FLANG_2:98
theorem :: FLANG_2:99
theorem :: FLANG_2:100
theorem :: FLANG_2:101
theorem :: FLANG_2:102
theorem :: FLANG_2:103
theorem :: FLANG_2:104
theorem Th105: :: FLANG_2:105
theorem :: FLANG_2:106
theorem :: FLANG_2:107
theorem :: FLANG_2:108
theorem :: FLANG_2:109
theorem :: FLANG_2:110
theorem :: FLANG_2:111
theorem :: FLANG_2:112
theorem :: FLANG_2:113
theorem :: FLANG_2:114
theorem :: FLANG_2:115
theorem :: FLANG_2:116
theorem :: FLANG_2:117