1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/props".
17 include "Lift/fwd.ma".
19 alias id "nplus_conf" = "cic:/matita/RELATIONAL/NPlus/props/nplus_conf.con".
21 axiom pippo: \forall x,y. x < y \to y <= x \to False.
23 theorem lift_conf: \forall q,h,d,t,x. Lift q h d t x \to
24 \forall y. Lift q h d t y \to
26 intros 6. elim H; clear H q h d t x;
27 [ lapply linear lift_sort_fwd to H1.
29 | lapply linear lift_lref_fwd to H1.
31 [ auto | destruct H1 | destruct H ]
32 | lapply linear lift_lref_fwd to H2.
34 [ destruct H | auto | lapply pippo to H1, H4. decompose ]
35 | lapply linear lift_lref_fwd to H3.
38 | lapply linear pippo to H5, H1. decompose
39 | lapply linear nplus_conf to H2, H4. subst. auto
43 theorem lift_ct_le: \forall q,h,d,t,y. (Lift q h d t y) \to
44 \forall k,e,x. (Lift q k e t x) \to
45 \forall z. (Lift q k e y z) \to
46 e <= d \to \forall d'. (k + d == d') \to
48 intros 6. elim H; clear H q h d t y;
49 [ lapply linear lift_sort_fwd to H1.
50 lapply linear lift_sort_fwd to H2.
52 | lapply linear lift_lref_fwd to H1.
53 lapply linear lift_lref_fwd to H2.