-theorem track_inv_impe: \forall P,r,S. Track P (impe r) S \to
- \exists Q,D,i. \exists a,b:Formula.
- S = pair (impl a b) D \land
- Track Q r (pair lleaf D) \land
- Insert (pair a b) i P Q.
- intros. inversion H; clear H; intros; subst. autobatch depth = 8 size = 10.
-qed.
-
-theorem track_inv_lleaf_impl:
- \forall Q,p,a,b. Track Q p (pair lleaf (impl a b)) \to
- (\exists P,i. p = lref i \land Insert (pair lleaf (impl a b)) i P Q) \lor
- (\exists r. p = impi r \land Track Q r (pair a b)).
- intros. inversion H; clear H; intros; subst;
- [ autobatch depth = 5
- | subst. autobatch depth = 4
- ].
-qed.
-(*
-theorem track_inv_impe: \forall P,p,q,r,S. Track P (impe p q r) S \to
+theorem track_inv_impi: \forall P,p,q,r,S. Track P (impi p q r) S \to