equal
deleted
inserted
replaced
33 adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool" |
33 adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool" |
34 "adm_wf R F == ALL f g x. |
34 "adm_wf R F == ALL f g x. |
35 (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x" |
35 (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x" |
36 |
36 |
37 wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" |
37 wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" |
38 "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y" |
38 [code func del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y" |
39 |
39 |
40 abbreviation acyclicP :: "('a => 'a => bool) => bool" where |
40 abbreviation acyclicP :: "('a => 'a => bool) => bool" where |
41 "acyclicP r == acyclic (Collect2 r)" |
41 "acyclicP r == acyclic (Collect2 r)" |
42 |
42 |
43 class wellorder = linorder + |
43 class wellorder = linorder + |