Thu, 13 Apr 1995 11:41:34 +0200 Redefined OUnion in a definitional manner, and proved the
lcp [Thu, 13 Apr 1995 11:41:34 +0200] rev 1038
Redefined OUnion in a definitional manner, and proved the rules again. Deleted the rules OUnionI/E as they were not needed. Proved OUN_cong. Extended OrdQuant_ss with oex_cong and defined Ord_atomize to extract rewrite rules from ALL x<i... assumptions.
Thu, 13 Apr 1995 11:40:07 +0200 Deleted lt_oadd_disj1
lcp [Thu, 13 Apr 1995 11:40:07 +0200] rev 1037
Deleted lt_oadd_disj1
Thu, 13 Apr 1995 11:38:48 +0200 Recoded function atomize so that new ways of creating
lcp [Thu, 13 Apr 1995 11:38:48 +0200] rev 1036
Recoded function atomize so that new ways of creating simplification rules can be added easily.
Thu, 13 Apr 1995 11:37:39 +0200 Proved Int_Diff_eq.
lcp [Thu, 13 Apr 1995 11:37:39 +0200] rev 1035
Proved Int_Diff_eq.
Thu, 13 Apr 1995 11:35:24 +0200 fixed typo
lcp [Thu, 13 Apr 1995 11:35:24 +0200] rev 1034
fixed typo
Thu, 13 Apr 1995 11:33:57 +0200 Defined ordinal difference, --
lcp [Thu, 13 Apr 1995 11:33:57 +0200] rev 1033
Defined ordinal difference, --
Thu, 13 Apr 1995 11:32:44 +0200 Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2,
lcp [Thu, 13 Apr 1995 11:32:44 +0200] rev 1032
Proved odiff_oadd_inverse, oadd_lt_cancel2, oadd_lt_iff2, odiff_lt_mono2. Deleted duplicate copy of oadd_le_mono.
(0) -1000 -300 -100 -30 -10 -7 +7 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip