equal
deleted
inserted
replaced
15 INCL :: "[i=>o]=>o" |
15 INCL :: "[i=>o]=>o" |
16 |
16 |
17 rules |
17 rules |
18 |
18 |
19 idgen_def |
19 idgen_def |
20 "idgen(f) == lam t.case(t,true,false,%x y.<f`x, f`y>,%u.lam x.f ` u(x))" |
20 "idgen(f) == lam t. case(t,true,false,%x y.<f`x, f`y>,%u. lam x. f ` u(x))" |
21 |
21 |
22 INCL_def "INCL(%x.P(x)) == (ALL f.(ALL n:Nat.P(f^n`bot)) --> P(fix(f)))" |
22 INCL_def "INCL(%x. P(x)) == (ALL f.(ALL n:Nat. P(f^n`bot)) --> P(fix(f)))" |
23 po_INCL "INCL(%x.a(x) [= b(x))" |
23 po_INCL "INCL(%x. a(x) [= b(x))" |
24 INCL_subst "INCL(P) ==> INCL(%x.P((g::i=>i)(x)))" |
24 INCL_subst "INCL(P) ==> INCL(%x. P((g::i=>i)(x)))" |
25 |
25 |
26 end |
26 end |