Library Top.IE_Property
This file is part of the IE library
Copyright (C) El Ouraoui, Mayero, Mazza
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
Ordre lexicographique sur les paires d'entiers
Inductive lex : (nat × nat) → (nat × nat) → Prop :=
| lt_L : ∀ s1 s2, (fst s1) < (fst s2) → lex s1 s2
| lt_G : ∀ s1 s2, (fst s1) = (fst s2) → (snd s1) < (snd s2)
→ lex s1 s2.
Notation "a <lex b" := (lex a b) (at level 70).
Definition f_cp t u := (eta ((t {0 := u })) ) + (eta u).
Definition alpha (t:term) (u:term) :=
((f_cp t u ),(num_occ t 0)).
| lt_L : ∀ s1 s2, (fst s1) < (fst s2) → lex s1 s2
| lt_G : ∀ s1 s2, (fst s1) = (fst s2) → (snd s1) < (snd s2)
→ lex s1 s2.
Notation "a <lex b" := (lex a b) (at level 70).
Definition f_cp t u := (eta ((t {0 := u })) ) + (eta u).
Definition alpha (t:term) (u:term) :=
((f_cp t u ),(num_occ t 0)).
Induction forte; preuve en cours
Axiom sn_ind :
∀ P : term → term → Prop,
(∀ t u:term,
(∀ t' u':term,
(alpha t' u') <lex (alpha t u) → P t' u')
→ (P t u) )
→ ∀ t u:term, P t u .
Lemma One_step_ls :
∀ t t' u,
(t [u]) -->ls (t' [u]) → num_occ t' 0 < num_occ t 0.
Lemma subst_var_0_eta :
∀ u,∀ i,
0 ≠ i → eta((TVar 0) {i := u}) = eta(TVar 0).
Lemma subst_var_eta :
∀ u,∀ n i,
i ≠ n → eta((TVar n) {i := u}) = eta (TVar n).