6 Hint discr : ltlc := Extern 4 (lt (weight_map (wadd ? ?) (lift (S ?) ? ?)) (wadd ? ? ?))
7 Simpl; Rewrite <- lift_weight_add_O.
9 Hint discr : ltlc := Extern 4 (lt (weight_map ? (lift (0) (0) ?)) ?)
12 Section lift_tlt_props. (*************************************************)
14 Theorem lift_weight_map: (t:?; h,d:?; f:?)
15 ((m:?) (le d m) -> (f m)=(0)) ->
16 (weight_map f (lift h d t)) = (weight_map f t).
21 Apply (lt_le_e n d); Intros.
23 Rewrite lift_bref_lt; XAuto.
24 (* case 2.2: n >= d *)
25 Rewrite lift_bref_ge; [ Simpl | XAuto ].
28 XElim k; Intros; LiftTailRw; Simpl.
30 XElim b; [ Rewrite H; [ Idtac | XAuto ] | Idtac | Idtac ];
31 Rewrite H0; Intros; Try (LeLtGen; Rewrite H2; Simpl); XAuto.
36 Hints Resolve lift_weight_map : ltlc.
38 Theorem lift_weight : (t:?; h,d:?) (weight (lift h d t)) = (weight t).
42 Theorem lift_weight_add : (w:?; t:?; h,d:?; f,g:?)
43 ((m:?) (lt m d) -> (g m) = (f m)) ->
45 ((m:?) (le d m) -> (g (S m)) = (f m)) ->
46 (weight_map f (lift h d t)) =
47 (weight_map g (lift (S h) d t)).
52 Apply (lt_le_e n d); Intros.
54 Repeat Rewrite lift_bref_lt; Simpl; XAuto.
55 (* case 2.2: n >= d *)
56 Repeat Rewrite lift_bref_ge; Simpl; Try Rewrite <- plus_n_Sm; XAuto.
58 XElim k; Intros; LiftTailRw; Simpl.
62 (Apply (f_equal2 nat nat); [ XAuto | Idtac ]);
63 ( Apply H0; Simpl; Intros; Try (LeLtGen; Rewrite H4; Simpl); XAuto).
68 Theorem lift_weight_add_O: (w:?; t:?; h:?; f:?)
69 (weight_map f (lift h (0) t)) =
70 (weight_map (wadd f w) (lift (S h) (0) t)).
72 EApply lift_weight_add; XAuto.
76 Theorem lift_tlt_dx: (k:?; u,t:?; h,d:?)
77 (tlt t (TTail k u (lift h d t))).
79 Rewrite <- (lift_weight t h d).
80 Fold (tlt (lift h d t) (TTail k u (lift h d t))); XAuto.
85 Hints Resolve lift_tlt_dx : ltlc.