:: Formal Languages -- Concatenation and Closure
:: by Micha{\l} Trybulec
::
:: Received March 9, 2007
:: Copyright (c) 2007 Association of Mizar Users
theorem Th1: :: FLANG_1:1
for
n1,
n,
n2 being
Nat st (
n1 > n or
n2 > n ) holds
n1 + n2 > n
theorem Th2: :: FLANG_1:2
for
n1,
n,
n2 being
Nat st
n1 + n <= n2 + 1 &
n > 0 holds
n1 <= n2
theorem Th3: :: FLANG_1:3
for
n1,
n2 being
Nat holds
(
n1 + n2 = 1 iff ( (
n1 = 1 &
n2 = 0 ) or (
n1 = 0 &
n2 = 1 ) ) )
theorem Th4: :: FLANG_1:4
theorem Th5: :: FLANG_1:5
theorem Th6: :: FLANG_1:6
theorem Th7: :: FLANG_1:7
theorem Th8: :: FLANG_1:8
theorem :: FLANG_1:9
theorem Th10: :: FLANG_1:10
theorem :: FLANG_1:11
theorem Th12: :: FLANG_1:12
:: deftheorem Def1 defines ^^ FLANG_1:def 1 :
theorem Th13: :: FLANG_1:13
theorem Th14: :: FLANG_1:14
theorem Th15: :: FLANG_1:15
theorem Th16: :: FLANG_1:16
theorem Th17: :: FLANG_1:17
theorem Th18: :: FLANG_1:18
theorem Th19: :: FLANG_1:19
theorem Th20: :: FLANG_1:20
theorem Th21: :: FLANG_1:21
theorem Th22: :: FLANG_1:22
theorem :: FLANG_1:23
:: deftheorem Def2 defines |^ FLANG_1:def 2 :
theorem Th24: :: FLANG_1:24
theorem Th25: :: FLANG_1:25
theorem Th26: :: FLANG_1:26
theorem Th27: :: FLANG_1:27
theorem Th28: :: FLANG_1:28
theorem Th29: :: FLANG_1:29
theorem :: FLANG_1:30
theorem Th31: :: FLANG_1:31
theorem :: FLANG_1:32
theorem Th33: :: FLANG_1:33
theorem Th34: :: FLANG_1:34
theorem :: FLANG_1:35
theorem Th36: :: FLANG_1:36
theorem :: FLANG_1:37
theorem Th38: :: FLANG_1:38
theorem :: FLANG_1:39
theorem :: FLANG_1:40
theorem Th41: :: FLANG_1:41
:: deftheorem defines * FLANG_1:def 3 :
theorem Th42: :: FLANG_1:42
theorem Th43: :: FLANG_1:43
theorem Th44: :: FLANG_1:44
theorem :: FLANG_1:45
theorem Th46: :: FLANG_1:46
theorem Th47: :: FLANG_1:47
theorem :: FLANG_1:48
theorem Th49: :: FLANG_1:49
theorem :: FLANG_1:50
theorem Th51: :: FLANG_1:51
theorem :: FLANG_1:52
theorem Th53: :: FLANG_1:53
theorem :: FLANG_1:54
theorem Th55: :: FLANG_1:55
theorem :: FLANG_1:56
theorem Th57: :: FLANG_1:57
theorem Th58: :: FLANG_1:58
theorem :: FLANG_1:59
theorem Th60: :: FLANG_1:60
theorem Th61: :: FLANG_1:61
theorem Th62: :: FLANG_1:62
theorem Th63: :: FLANG_1:63
theorem :: FLANG_1:64
theorem :: FLANG_1:65
theorem Th66: :: FLANG_1:66
theorem :: FLANG_1:67
theorem Th68: :: FLANG_1:68
theorem Th69: :: FLANG_1:69
theorem :: FLANG_1:70
theorem :: FLANG_1:71
theorem :: FLANG_1:72
theorem Th73: :: FLANG_1:73
:: deftheorem Def4 defines Lex FLANG_1:def 4 :
theorem Th74: :: FLANG_1:74
theorem :: FLANG_1:75
theorem :: FLANG_1:76