21 inductive |
21 inductive |
22 domains "Ssub" <= "redexes*redexes" |
22 domains "Ssub" <= "redexes*redexes" |
23 intrs |
23 intrs |
24 Sub_Var "n:nat ==> Var(n)<== Var(n)" |
24 Sub_Var "n:nat ==> Var(n)<== Var(n)" |
25 Sub_Fun "[|u<== v|]==> Fun(u)<== Fun(v)" |
25 Sub_Fun "[|u<== v|]==> Fun(u)<== Fun(v)" |
26 Sub_App1 "[|u1<== v1; u2<== v2; b:bool|]==> \ |
26 Sub_App1 "[|u1<== v1; u2<== v2; b:bool|]==> |
27 \ App(0,u1,u2)<== App(b,v1,v2)" |
27 App(0,u1,u2)<== App(b,v1,v2)" |
28 Sub_App2 "[|u1<== v1; u2<== v2|]==> \ |
28 Sub_App2 "[|u1<== v1; u2<== v2|]==> |
29 \ App(1,u1,u2)<== App(1,v1,v2)" |
29 App(1,u1,u2)<== App(1,v1,v2)" |
30 type_intrs "redexes.intrs@bool_typechecks" |
30 type_intrs "redexes.intrs@bool_typechecks" |
31 |
31 |
32 inductive |
32 inductive |
33 domains "Scomp" <= "redexes*redexes" |
33 domains "Scomp" <= "redexes*redexes" |
34 intrs |
34 intrs |
35 Comp_Var "n:nat ==> Var(n) ~ Var(n)" |
35 Comp_Var "n:nat ==> Var(n) ~ Var(n)" |
36 Comp_Fun "[|u ~ v|]==> Fun(u) ~ Fun(v)" |
36 Comp_Fun "[|u ~ v|]==> Fun(u) ~ Fun(v)" |
37 Comp_App "[|u1 ~ v1; u2 ~ v2; b1:bool; b2:bool|]==> \ |
37 Comp_App "[|u1 ~ v1; u2 ~ v2; b1:bool; b2:bool|]==> |
38 \ App(b1,u1,u2) ~ App(b2,v1,v2)" |
38 App(b1,u1,u2) ~ App(b2,v1,v2)" |
39 type_intrs "redexes.intrs@bool_typechecks" |
39 type_intrs "redexes.intrs@bool_typechecks" |
40 |
40 |
41 inductive |
41 inductive |
42 domains "Sreg" <= "redexes" |
42 domains "Sreg" <= "redexes" |
43 intrs |
43 intrs |
44 Reg_Var "n:nat ==> regular(Var(n))" |
44 Reg_Var "n:nat ==> regular(Var(n))" |
45 Reg_Fun "[|regular(u)|]==> regular(Fun(u))" |
45 Reg_Fun "[|regular(u)|]==> regular(Fun(u))" |
46 Reg_App1 "[|regular(Fun(u)); regular(v) \ |
46 Reg_App1 "[|regular(Fun(u)); regular(v) |
47 \ |]==>regular(App(1,Fun(u),v))" |
47 |]==>regular(App(1,Fun(u),v))" |
48 Reg_App2 "[|regular(u); regular(v) \ |
48 Reg_App2 "[|regular(u); regular(v) |
49 \ |]==>regular(App(0,u,v))" |
49 |]==>regular(App(0,u,v))" |
50 type_intrs "redexes.intrs@bool_typechecks" |
50 type_intrs "redexes.intrs@bool_typechecks" |
51 |
51 |
52 defs |
52 defs |
53 union_def "u un v == redex_rec(u, \ |
53 union_def "u un v == redex_rec(u, |
54 \ %i.lam t:redexes.redexes_case(%j.Var(i), %x.0, %b x y.0, t), \ |
54 %i.lam t:redexes.redexes_case(%j.Var(i), %x.0, %b x y.0, t), |
55 \ %x m.lam t:redexes.redexes_case(%j.0, %y.Fun(m`y), %b y z.0, t), \ |
55 %x m.lam t:redexes.redexes_case(%j.0, %y.Fun(m`y), %b y z.0, t), |
56 \%b x y m p.lam t:redexes.redexes_case(%j.0, %y.0, \ |
56 %b x y m p.lam t:redexes.redexes_case(%j.0, %y.0, |
57 \ %c z u. App(b or c, m`z, p`u), t))`v" |
57 %c z u. App(b or c, m`z, p`u), t))`v" |
58 end |
58 end |
59 |
59 |