]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambda_delta/Basic_2/functional/rtm_step.ma
- main lemmas about abstract reducibility candidates closed
[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / functional / rtm_step.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "Basic_2/functional/rtm.ma".
16
17 (* REDUCTION AND TYPE MACHINE ***********************************************)
18
19 (* transitions *)
20 inductive rtm_step: relation rtm ≝
21 | rtm_ldrop : ∀G,u,E,I,t,F,V,S,i.
22               rtm_step (mk_rtm G u (E. ④{I} {t, F, V}) S (#(i + 1)))
23                        (mk_rtm G u E S (#i))
24 | rtm_ldelta: ∀G,u,E,t,F,V,S.
25               rtm_step (mk_rtm G u (E. ④{Abbr} {t, F, V}) S (#0))
26                        (mk_rtm G u F S V)
27 | rtm_ltype : ∀G,u,E,t,F,V,S.
28               rtm_step (mk_rtm G u (E. ④{Abst} {t, F, V}) S (#0))
29                        (mk_rtm G u F S V)
30 | rtm_gdrop : ∀G,I,V,u,E,S,p. p < |G| →
31               rtm_step (mk_rtm (G. ⓑ{I} V) u E S (§p))
32                        (mk_rtm G u E S (§p))
33 | rtm_gdelta: ∀G,V,u,E,S,p. p = |G| →
34               rtm_step (mk_rtm (G. ⓓV) u E S (§p))
35                        (mk_rtm G u E S V)
36 | rtm_gtype : ∀G,V,u,E,S,p. p = |G| →
37               rtm_step (mk_rtm (G. ⓛV) u E S (§p))
38                        (mk_rtm G u E S V)
39 | rtm_tau   : ∀G,u,E,S,W,T.
40               rtm_step (mk_rtm G u E S (ⓣW. T))
41                        (mk_rtm G u E S T)
42 | rtm_appl  : ∀G,u,E,S,V,T.
43               rtm_step (mk_rtm G u E S (ⓐV. T))
44                        (mk_rtm G u E ({E, V} :: S) T)
45 | rtm_beta  : ∀G,u,E,F,V,S,W,T.
46               rtm_step (mk_rtm G u E ({F, V} :: S) (ⓛW. T))
47                        (mk_rtm G u (E. ④{Abbr} {u, F, V}) S T)
48 | rtm_push  : ∀G,u,E,W,T.
49               rtm_step (mk_rtm G u E ⟠ (ⓛW. T))
50                        (mk_rtm G (u + 1) (E. ④{Abst} {u, E, W}) ⟠ T)
51 | rtm_theta : ∀G,u,E,S,V,T.
52               rtm_step (mk_rtm G u E S (ⓓV. T))
53                        (mk_rtm G u (E. ④{Abbr} {u, E, V}) S T)
54 .
55
56 interpretation "sequential reduction (RTM)"
57    'SRed O1 O2 = (rtm_step O1 O2).