]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambda_delta/Basic_2/grammar/term_simple.ma
- first properties of strongly normalizing terms
[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / grammar / term_simple.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/grammar/term.ma".
16
17 (* SIMPLE (NEUTRAL) TERMS ***************************************************)
18
19 inductive simple: predicate term ≝
20    | simple_atom: ∀I. simple (⓪{I})
21    | simple_flat: ∀I,V,T. simple (ⓕ{I} V. T)
22 .
23
24 interpretation "simple (term)" 'Simple T = (simple T).
25
26 (* Basic inversion lemmas ***************************************************)
27
28 fact simple_inv_bind_aux: ∀T. 𝐒[T] → ∀J,W,U. T = ⓑ{J} W. U → False.
29 #T * -T
30 [ #I #J #W #U #H destruct
31 | #I #V #T #J #W #U #H destruct
32 ]
33 qed.
34
35 lemma simple_inv_bind: ∀I,V,T. 𝐒[ⓑ{I} V. T] → False.
36 /2 width=6/ qed-.