equal
deleted
inserted
replaced
1143 ML{*ResAtp.problem_name:="BigO__bigo_lesso1"*} |
1143 ML{*ResAtp.problem_name:="BigO__bigo_lesso1"*} |
1144 lemma bigo_lesso1: "ALL x. f x <= g x ==> f <o g =o O(h)" |
1144 lemma bigo_lesso1: "ALL x. f x <= g x ==> f <o g =o O(h)" |
1145 apply (unfold lesso_def) |
1145 apply (unfold lesso_def) |
1146 apply (subgoal_tac "(%x. max (f x - g x) 0) = 0") |
1146 apply (subgoal_tac "(%x. max (f x - g x) 0) = 0") |
1147 (*??Translation of TSTP raised an exception: Type unification failed: Variable ?'X2.0::type not of sort ord*) |
1147 (*??Translation of TSTP raised an exception: Type unification failed: Variable ?'X2.0::type not of sort ord*) |
1148 apply (metis bigo_zero ord_class.max) |
1148 apply (metis bigo_zero) |
1149 apply (unfold func_zero) |
1149 apply (unfold func_zero) |
1150 apply (rule ext) |
1150 apply (rule ext) |
1151 apply (simp split: split_max) |
1151 apply (simp split: split_max) |
1152 done |
1152 done |
1153 |
1153 |