/3 width=5 by fpb_lpx, fpbs_strap1/
qed.
-lemma lleq_fpbs: â\88\80h,g,G,L1,L2,T. L1 â\8b\95[T, 0] L2 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄.
+lemma lleq_fpbs: â\88\80h,g,G,L1,L2,T. L1 â\89¡[T, 0] L2 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄.
/3 width=1 by fpb_fpbs, fpb_lleq/ qed.
lemma cprs_fpbs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄.
qed-.
lemma fpbs_lleq_trans: ∀h,g,G1,G,L1,L,L2,T1,T. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ →
- L â\8b\95[T, 0] L2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L2, T⦄.
+ L â\89¡[T, 0] L2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L2, T⦄.
/3 width=5 by fpbs_strap1, fpb_lleq/ qed-.
lemma fqus_fpbs_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ →
qed-.
lemma lleq_fpbs_trans: ∀h,g,G1,G2,L1,L,L2,T1,T2. ⦃G1, L, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ →
- L1 â\8b\95[T1, 0] L → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+ L1 â\89¡[T1, 0] L → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
/3 width=5 by fpbs_strap2, fpb_lleq/ qed-.
lemma cpxs_fqus_fpbs: ∀h,g,G1,G2,L1,L2,T1,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T →