equal
deleted
inserted
replaced
21 rules |
21 rules |
22 |
22 |
23 (*** Definitions of Hereditary Termination ***) |
23 (*** Definitions of Hereditary Termination ***) |
24 |
24 |
25 HTTgen_def |
25 HTTgen_def |
26 "HTTgen(R) == {t. t=true | t=false | (EX a b.t=<a,b> & a : R & b : R) | \ |
26 "HTTgen(R) == {t. t=true | t=false | (EX a b.t=<a,b> & a : R & b : R) | |
27 \ (EX f. t=lam x.f(x) & (ALL x.f(x) : R))}" |
27 (EX f. t=lam x.f(x) & (ALL x.f(x) : R))}" |
28 HTT_def "HTT == gfp(HTTgen)" |
28 HTT_def "HTT == gfp(HTTgen)" |
29 |
29 |
30 end |
30 end |