:: A Theory of Sequential Files
:: by Hirofumi Fukura and Yatsuka Nakamura
::
:: Received August 12, 2005
:: Copyright (c) 2005 Association of Mizar Users
theorem Th1: :: FILEREC1:1
theorem Th2: :: FILEREC1:2
theorem Th3: :: FILEREC1:3
theorem Th4: :: FILEREC1:4
theorem Th5: :: FILEREC1:5
theorem Th6: :: FILEREC1:6
theorem :: FILEREC1:7
theorem :: FILEREC1:8
theorem :: FILEREC1:9
theorem Th10: :: FILEREC1:10
theorem :: FILEREC1:11
theorem :: FILEREC1:12
theorem :: FILEREC1:13
theorem Th14: :: FILEREC1:14
theorem :: FILEREC1:15
theorem :: FILEREC1:16
theorem :: FILEREC1:17
theorem Th18: :: FILEREC1:18
theorem Th19: :: FILEREC1:19
theorem :: FILEREC1:20
canceled;
theorem :: FILEREC1:21
:: deftheorem Def1 defines is_a_record_of FILEREC1:def 1 :
theorem Th22: :: FILEREC1:22
theorem Th23: :: FILEREC1:23
theorem :: FILEREC1:24
theorem Th25: :: FILEREC1:25
theorem :: FILEREC1:26
theorem Th27: :: FILEREC1:27
theorem Th28: :: FILEREC1:28
theorem Th29: :: FILEREC1:29
theorem :: FILEREC1:30
theorem Th31: :: FILEREC1:31
theorem Th32: :: FILEREC1:32
theorem :: FILEREC1:33
theorem :: FILEREC1:34
theorem Th35: :: FILEREC1:35
theorem Th36: :: FILEREC1:36
theorem Th37: :: FILEREC1:37
theorem Th38: :: FILEREC1:38
theorem :: FILEREC1:39
theorem Th40: :: FILEREC1:40
theorem Th41: :: FILEREC1:41
theorem Th42: :: FILEREC1:42
theorem :: FILEREC1:43
theorem :: FILEREC1:44
theorem :: FILEREC1:45