19 |
19 |
20 |
20 |
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 |
35 one_step "[|m-1->n|] ==> m--->n" |
35 one_step "[|m-1->n|] ==> m--->n" |
36 refl "m:lambda==>m --->m" |
36 refl "m:lambda==>m --->m" |
37 trans "[|m--->n; n--->p|]==>m--->p" |
37 trans "[|m--->n; n--->p|]==>m--->p" |
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 |
54 one_step "[|m =1=> n|] ==> m ===> n" |
54 one_step "[|m =1=> n|] ==> m ===> n" |
55 trans "[|m===>n; n===>p|]==>m===>p" |
55 trans "[|m===>n; n===>p|]==>m===>p" |
56 type_intrs "[Spar_red1.dom_subset RS subsetD]@red_typechecks" |
56 type_intrs "[Spar_red1.dom_subset RS subsetD]@red_typechecks" |
57 |
57 |
58 |
58 |
59 end |
59 end |
60 |
60 |