]> matita.cs.unibo.it Git - helm.git/blob - matita/contribs/LOGIC/Track/pred.ma
c7f6198f95f01e9fedcefdce6c33504223a60892
[helm.git] / matita / contribs / LOGIC / Track / pred.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 set "baseuri" "cic:/matita/LOGIC/Track/pred".
16
17 (**)
18
19 include "Track/inv.ma".
20 include "PRed/defs.ma".
21
22 theorem track_pred: \forall Q1,Q2,p1,p2,S1,S2. PRed Q1 p1 S1 Q2 p2 S2 \to
23                     Track Q1 p1 S1 \to Track Q2 p2 S2.
24  intros 7; elim H; clear H Q1 Q2 p1 p2 S1 S2;
25  [ autobatch
26  | autobatch
27  | lapply linear track_inv_impw to H3; decompose; subst; autobatch
28  | lapply linear track_inv_impr to H3; decompose; subst; autobatch
29  | lapply linear track_inv_impi to H7; decompose; subst; autobatch size = 7
30  | lapply linear track_inv_scut to H5; decompose; subst; autobatch
31  | lapply linear track_inv_scut to H4; decompose; subst;
32    lapply linear track_inv_lref to H6; decompose; autobatch
33  | lapply linear track_inv_scut to H4; decompose; subst;
34    lapply linear track_inv_lref to H5; decompose; autobatch
35  | lapply linear track_inv_scut to H3; decompose; subst;
36    lapply linear track_inv_prin to H5; subst; autobatch
37  | lapply linear track_inv_scut to H3; decompose; subst;
38    lapply linear track_inv_prin to H4; subst; autobatch
39  | lapply linear track_inv_scut to H3; decompose; subst;
40    lapply linear track_inv_impw to H4; decompose; subst;
41    lapply linear track_inv_impr to H5; decompose; subst; autobatch
42  ].
43 qed.