equal
deleted
inserted
replaced
15 the_recfun :: "[('a * 'a)set, 'a, ['a,'a=>'b]=>'b] => 'a=>'b" |
15 the_recfun :: "[('a * 'a)set, 'a, ['a,'a=>'b]=>'b] => 'a=>'b" |
16 |
16 |
17 defs |
17 defs |
18 wf_def "wf(r) == (!P. (!x. (!y. <y,x>:r --> P(y)) --> P(x)) --> (!x.P(x)))" |
18 wf_def "wf(r) == (!P. (!x. (!y. <y,x>:r --> P(y)) --> P(x)) --> (!x.P(x)))" |
19 |
19 |
20 cut_def "cut f r x == (%y. if (<y,x>:r) (f y) (@z.True))" |
20 cut_def "cut f r x == (%y. if <y,x>:r then f y else @z.True)" |
21 |
21 |
22 is_recfun_def "is_recfun r a H f == (f = cut (%x.(H x (cut f r x))) r a)" |
22 is_recfun_def "is_recfun r a H f == (f = cut (%x.(H x (cut f r x))) r a)" |
23 |
23 |
24 the_recfun_def "the_recfun r a H == (@f.is_recfun r a H f)" |
24 the_recfun_def "the_recfun r a H == (@f.is_recfun r a H f)" |
25 |
25 |