7 Section subst0_tlt_props. (***********************************************)
9 Theorem subst0_weight_le : (u,t,z:?; d:?) (subst0 d u t z) ->
10 (f,g:?) ((m:?) (le (f m) (g m))) ->
11 (lt (weight_map f (lift (S d) (0) u)) (g d)) ->
12 (le (weight_map f z) (weight_map g t)).
13 Intros until 1; XElim H.
14 (* case 1: subst0_lref *)
16 (* case 2: subst0_fst *)
17 XElim k; [ XElim b | Idtac ]; Simpl; [ Auto 7 with ltlc (**) | XAuto | XAuto | XAuto ].
18 (* case 3: subst0_snd *)
19 XElim k; [ XElim b | Idtac ]; Simpl; [ Auto 7 with ltlc (**) | XAuto | XAuto | XAuto ].
20 (* case 4: subst0_both *)
21 XElim k; [ XElim b | Idtac ]; Simpl; [ Auto 7 with ltlc (**) | XAuto | XAuto | XAuto ].
24 Theorem subst0_weight_lt : (u,t,z:?; d:?) (subst0 d u t z) -> (f,g:?)
25 ((m:?) (le (f m) (g m))) ->
26 (lt (weight_map f (lift (S d) (0) u)) (g d)) ->
27 (lt (weight_map f z) (weight_map g t)).
28 Intros until 1; XElim H.
29 (* case 1: subst0_lref *)
31 (* case 2: subst0_fst *)
32 XElim k; [ XElim b | Idtac ]; Simpl; Intros;
33 Apply lt_n_S; (Apply lt_le_plus_plus; [ XAuto | Idtac ]); (**)
34 [ Auto 6 with ltlc (**) | XAuto | XAuto | XAuto ].
35 (* case 3: subst0_snd *)
36 XElim k; [ XElim b | Idtac ]; Simpl;
37 [ Auto 8 with ltlc | Auto 6 with ltlc | Auto 6 with ltlc | XAuto ]. (**)
38 (* case 3: subst0_both *)
39 XElim k; [ XElim b | Idtac ]; Simpl;
40 Intros; Apply lt_n_S; [ Apply lt_le_plus_plus | Apply lt_plus_plus | Apply lt_plus_plus | Apply lt_plus_plus ]; XAuto.
41 EApply subst0_weight_le; [ XEAuto | XAuto | XAuto ].
44 Theorem subst0_tlt_tail: (u,t,z:?) (subst0 (0) u t z) ->
45 (tlt (TTail (Bind Abbr) u z)
46 (TTail (Bind Abbr) u t)
48 Unfold tlt weight; Intros; Simpl.
49 Apply lt_n_S; Apply le_lt_plus_plus; [ XAuto | Idtac ].
50 EApply subst0_weight_lt; [ XEAuto | XAuto | XAuto ].
53 Theorem subst0_tlt: (u,t,z:?) (subst0 (0) u t z) ->
54 (tlt z (TTail (Bind Abbr) u t)).
56 EApply tlt_trans; [ Idtac | Apply subst0_tlt_tail; XEAuto].
62 Hints Resolve subst0_tlt : ltlc.