equal
deleted
inserted
replaced
21 inductive |
21 inductive |
22 domains "Sred1" <= "lambda*lambda" |
22 domains "Sred1" <= "lambda*lambda" |
23 intrs |
23 intrs |
24 beta "[|m:lambda; n:lambda|] ==> Apl(Fun(m),n) -1-> n/m" |
24 beta "[|m:lambda; n:lambda|] ==> Apl(Fun(m),n) -1-> n/m" |
25 rfun "[|m -1-> n|] ==> Fun(m) -1-> Fun(n)" |
25 rfun "[|m -1-> n|] ==> Fun(m) -1-> Fun(n)" |
26 apl_l "[|m2:lambda; m1 -1-> n1|] ==> \ |
26 apl_l "[|m2:lambda; m1 -1-> n1|] ==> |
27 \ Apl(m1,m2) -1-> Apl(n1,m2)" |
27 Apl(m1,m2) -1-> Apl(n1,m2)" |
28 apl_r "[|m1:lambda; m2 -1-> n2|] ==> \ |
28 apl_r "[|m1:lambda; m2 -1-> n2|] ==> |
29 \ Apl(m1,m2) -1-> Apl(m1,n2)" |
29 Apl(m1,m2) -1-> Apl(m1,n2)" |
30 type_intrs "red_typechecks" |
30 type_intrs "red_typechecks" |
31 |
31 |
32 inductive |
32 inductive |
33 domains "Sred" <= "lambda*lambda" |
33 domains "Sred" <= "lambda*lambda" |
34 intrs |
34 intrs |
38 type_intrs "[Sred1.dom_subset RS subsetD]@red_typechecks" |
38 type_intrs "[Sred1.dom_subset RS subsetD]@red_typechecks" |
39 |
39 |
40 inductive |
40 inductive |
41 domains "Spar_red1" <= "lambda*lambda" |
41 domains "Spar_red1" <= "lambda*lambda" |
42 intrs |
42 intrs |
43 beta "[|m =1=> m'; \ |
43 beta "[|m =1=> m'; |
44 \ n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'" |
44 n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'" |
45 rvar "n:nat==> Var(n) =1=> Var(n)" |
45 rvar "n:nat==> Var(n) =1=> Var(n)" |
46 rfun "[|m =1=> m'|]==> Fun(m) =1=> Fun(m')" |
46 rfun "[|m =1=> m'|]==> Fun(m) =1=> Fun(m')" |
47 rapl "[|m =1=> m'; \ |
47 rapl "[|m =1=> m'; |
48 \ n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')" |
48 n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')" |
49 type_intrs "red_typechecks" |
49 type_intrs "red_typechecks" |
50 |
50 |
51 inductive |
51 inductive |
52 domains "Spar_red" <= "lambda*lambda" |
52 domains "Spar_red" <= "lambda*lambda" |
53 intrs |
53 intrs |