begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem
theorem
theorem
theorem Th10:
theorem
theorem
theorem
theorem Th14:
theorem
theorem
theorem
theorem Th18:
theorem Th19:
theorem
canceled;
theorem
:: deftheorem Def1 defines is_a_record_of FILEREC1:def 1 :
theorem Th22:
theorem Th23:
theorem
theorem Th25:
theorem
theorem Th27:
theorem Th28:
theorem Th29:
theorem
theorem Th31:
theorem Th32:
theorem
theorem
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem
theorem Th40:
theorem Th41:
theorem Th42:
theorem
theorem
theorem