15 translations |
15 translations |
16 "lift(r)" == "lift_rec(r,0)" |
16 "lift(r)" == "lift_rec(r,0)" |
17 "u/v" == "subst_rec(u,v,0)" |
17 "u/v" == "subst_rec(u,v,0)" |
18 |
18 |
19 defs |
19 defs |
20 lift_rec_def "lift_rec(r,kg) == \ |
20 lift_rec_def "lift_rec(r,kg) == |
21 \ redex_rec(r,%i.(lam k:nat.if(i<k,Var(i),Var(succ(i)))), \ |
21 redex_rec(r,%i.(lam k:nat.if(i<k,Var(i),Var(succ(i)))), |
22 \ %x m.(lam k:nat.Fun(m`(succ(k)))), \ |
22 %x m.(lam k:nat.Fun(m`(succ(k)))), |
23 \ %b x y m p.lam k:nat.App(b,m`k,p`k))`kg" |
23 %b x y m p.lam k:nat.App(b,m`k,p`k))`kg" |
24 |
24 |
25 |
25 |
26 (* subst_rec(u,Var(i),k) = if k<i then Var(i-1) |
26 (* subst_rec(u,Var(i),k) = if k<i then Var(i-1) |
27 else if k=i then u |
27 else if k=i then u |
28 else Var(i) |
28 else Var(i) |
29 subst_rec(u,Fun(t),k) = Fun(subst_rec(lift(u),t,succ(k))) |
29 subst_rec(u,Fun(t),k) = Fun(subst_rec(lift(u),t,succ(k))) |
30 subst_rec(u,App(b,f,a),k) = App(b,subst_rec(u,f,p),subst_rec(u,a,p)) |
30 subst_rec(u,App(b,f,a),k) = App(b,subst_rec(u,f,p),subst_rec(u,a,p)) |
31 |
31 |
32 *) |
32 *) |
33 subst_rec_def "subst_rec(u,t,kg) == \ |
33 subst_rec_def "subst_rec(u,t,kg) == |
34 \ redex_rec(t, \ |
34 redex_rec(t, |
35 \ %i.(lam r:redexes.lam k:nat. \ |
35 %i.(lam r:redexes.lam k:nat. |
36 \ if(k<i,Var(i#-1), \ |
36 if(k<i,Var(i#-1), |
37 \ if(k=i,r,Var(i)))), \ |
37 if(k=i,r,Var(i)))), |
38 \ %x m.(lam r:redexes.lam k:nat. \ |
38 %x m.(lam r:redexes.lam k:nat. |
39 \ Fun(m`(lift(r))`(succ(k)))), \ |
39 Fun(m`(lift(r))`(succ(k)))), |
40 \ %b x y m p.lam r:redexes.lam k:nat. \ |
40 %b x y m p.lam r:redexes.lam k:nat. |
41 \ App(b,m`r`k,p`r`k))`u`kg" |
41 App(b,m`r`k,p`r`k))`u`kg" |
42 |
42 |
43 |
43 |
44 end |
44 end |
45 |
45 |
46 |
46 |