(* *)
(**************************************************************************)
-include "basic_2/static/ffdeq_fqus.ma".
-include "basic_2/static/ffdeq_ffdeq.ma".
+include "static_2/static/fdeq_fqus.ma".
+include "static_2/static/fdeq_fdeq.ma".
include "basic_2/rt_computation/cpxs_fqus.ma".
-include "basic_2/rt_computation/cpxs_ffdeq.ma".
-include "basic_2/rt_computation/lpxs_ffdeq.ma".
-include "basic_2/rt_computation/lpxs_lpx.ma".
-include "basic_2/rt_computation/fpbs_fqus.ma".
+include "basic_2/rt_computation/cpxs_fdeq.ma".
+include "basic_2/rt_computation/lpxs_fdeq.ma".
include "basic_2/rt_computation/fpbs_cpxs.ma".
(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************)
qed-.
(* Basic_2A1: uses: lpxs_lleq_fpbs *)
-lemma lpxs_ffdeq_fpbs: ∀h,o,G1,L1,L,T1. ⦃G1, L1⦄ ⊢ ⬈*[h] L →
- ∀G2,L2,T2. ⦃G1, L, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
-/3 width=3 by lpxs_fpbs_trans, ffdeq_fpbs/ qed.
+lemma lpxs_fdeq_fpbs: ∀h,o,G1,L1,L,T1. ⦃G1, L1⦄ ⊢ ⬈*[h] L →
+ ∀G2,L2,T2. ⦃G1, L, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
+/3 width=3 by lpxs_fpbs_trans, fdeq_fpbs/ qed.
lemma fpbs_lpx_trans: ∀h,o,G1,G2,L1,L,T1,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L, T2⦄ →
∀L2. ⦃G2, L⦄ ⊢ ⬈[h] L2 → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
∀G,L,T0. ⦃G1, L1, T⦄ ⊐* ⦃G, L, T0⦄ →
∀L0. ⦃G, L⦄ ⊢ ⬈*[h] L0 →
∀G2,L2,T2. ⦃G, L0, T0⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ .
-/3 width=5 by cpxs_fqus_lpxs_fpbs, fpbs_strap1, fpbq_ffdeq/ qed.
+/3 width=5 by cpxs_fqus_lpxs_fpbs, fpbs_strap1, fpbq_fdeq/ qed.
(* Advanced inversion lemmas *************************************************)
elim (lpx_fqus_trans … H34 … HL10) -L0
/3 width=9 by lpxs_step_sn, cpxs_trans, ex4_5_intro/
| #G0 #L0 #T0 #H10 #_ * #G3 #L3 #L4 #T3 #T4 #HT03 #H34 #HL34 #H42
- elim (ffdeq_cpxs_trans … H10 … HT03) -T0 #T0 #HT10 #H03
- elim (ffdeq_fqus_trans … H03 … H34) -G0 -L0 -T3 #G0 #L0 #T3 #H03 #H34
- elim (ffdeq_lpxs_trans … H34 … HL34) -L3 #L3 #HL03 #H34
- /3 width=13 by ffdeq_trans, ex4_5_intro/
+ elim (fdeq_cpxs_trans … H10 … HT03) -T0 #T0 #HT10 #H03
+ elim (fdeq_fqus_trans … H03 … H34) -G0 -L0 -T3 #G0 #L0 #T3 #H03 #H34
+ elim (fdeq_lpxs_trans … H34 … HL34) -L3 #L3 #HL03 #H34
+ /3 width=13 by fdeq_trans, ex4_5_intro/
]
]
qed-.