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 (**************************************************************************)
17 include "Track/defs.ma".
19 (* Main inversion lemmas ****************************************************)
21 theorem track_inv_lref: \forall Q,S,i. Track Q (lref i) S \to
22 \exists p1,p2,P. Insert p1 p2 S i P Q.
23 intros; inversion H; clear H; intros; destruct; autobatch depth = 4.
26 theorem track_inv_prin: \forall P,S,h. Track P (prin h) S \to
27 S = pair (posr h) (posr h).
28 intros; inversion H; clear H; intros; destruct; autobatch.
31 theorem track_inv_impw: \forall P,p,S. Track P (impw p) S \to
33 S = pair (impl a b) B \land
34 Track P p (pair lleaf B).
35 intros; inversion H; clear H; intros; destruct; autobatch depth = 5.
38 theorem track_inv_impr: \forall Q,p,S. Track Q (impr p) S \to
40 S = pair lleaf (impl a b) \land
42 intros; inversion H; clear H; intros; destruct; autobatch depth = 4.
45 theorem track_inv_impi: \forall P,p,q,r,S. Track P (impi p q r) S \to
46 \exists A,B,D. \exists a,b:Formula.
47 S = pair (impl a b) D \land
48 Track P p (pair A a) \land
49 Track P q (pair b B) \land
50 Track (abst P p q (pair A B)) r (pair lleaf D).
51 intros; inversion H; clear H; intros; destruct; autobatch depth = 9 width = 4 size = 12.
54 theorem track_inv_scut: \forall P,q,r,S. Track P (scut q r) S \to
55 \exists A,B. \exists c:Formula.
57 Track P q (pair A c) \land
59 intros; inversion H; clear H; intros; destruct; autobatch depth = 6 size = 8.