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/LOGIC/Track/order".
17 include "Track/props.ma".
19 (* Order properties *********************************************************)
21 theorem track_refl: \forall P. \forall c:Formula. \exists r.
23 intros. elim c; clear c;
25 | lapply (insert_total (pair f f1) zero P); [2:autobatch];
26 decompose. autobatch depth = 5
30 theorem track_trans: \forall p,q,A,B. \forall c:Formula.
31 Track leaf p (pair A c) \to Track leaf q (pair c B) \to
32 \exists r. Track leaf r (pair A B).
33 intros 1; elim p names 0; clear p;
35 lapply linear track_inv_lref to H. decompose.
36 lapply insert_inv_leaf_2 to H. decompose
38 lapply linear track_inv_parx to H. subst. autobatch.
40 lapply linear track_inv_impw to H1.
42 lapply linear H to H4, H2. decompose. autobatch
43 | intros 3. elim q; clear q;
45 lapply linear track_inv_lref to H2. decompose.
46 lapply insert_inv_leaf_2 to H. decompose
47 | lapply linear track_inv_parx to H2. subst. autobatch
49 lapply linear track_inv_impi to H2.
50 lapply linear track_inv_impw to H3.
51 decompose. subst. autobatch
53 lapply linear track_inv_impi to H3.
56 lapply linear track_inv_impi to H2.
57 lapply linear track_inv_impe to H3.
58 decompose. subst. autobatch
60 | intros 3. elim q; clear q;
62 lapply linear track_inv_lref to H2. decompose.
63 lapply insert_inv_leaf_2 to H. decompose
65 lapply linear track_inv_parx to H2.
68 lapply linear track_inv_impe to H2.
69 lapply linear track_inv_impw to H3.
70 decompose. subst. autobatch
72 lapply linear track_inv_impi to H3. decompose. subst
74 lapply linear track_inv_impe to H2.
75 lapply linear track_inv_impe to H3.
77 lapply linear track_inv_lleaf_impl to H5. decompose; subst;
79 lapply linear insert_inv_leaf_1 to H3. decompose. subst.
80 lapply linear insert_inv_abst_2 to H2. decompose. subst
81 | lapply insert_conf to H3, H4. clear H4. decompose.
82 lapply linear track_weak to H6, H4. decompose.
83 lapply linear track_comp to H2, H, H1. decompose. autobatch
89 | lapply linear track_inv_impi to H4.
90 lapply linear track_inv_impe to H5.
92 destruct H4. destruct H5. clear H4 H5. subst.
93 unfold linj in Hcut. unfold rinj in Hcut3. destruct Hcut. destruct Hcut3. clear Hcut Hcut3. subst.
94 destruct Hcut2. clear Hcut2. subst.