---

Step * 1 of Lemma permr_upto_functionality_wrt_permr_upto


1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. EquivRel(T;x,y.R[x;y])
⊢ ∀as,as',bs,bs':T List.
    (as ≡ bs upto x,y.R[x;y] 
    ⇒ as' ≡ bs' upto x,y.R[x;y] 
    ⇒ (as ≡ as' upto x,y.R[x;y]  ⇐⇒ bs ≡ bs' upto x,y.R[x;y] ))
BY
{ ((BLemma `equiv_rel_self_functionality` THENM BLemma `permr_upto_equiv_rel`) THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  EquivRel(T;x,y.R[x;y])
\mvdash{}  \mforall{}as,as',bs,bs':T  List.
        (as  \mequiv{}  bs  upto  x,y.R[x;y] 
        {}\mRightarrow{}  as'  \mequiv{}  bs'  upto  x,y.R[x;y] 
        {}\mRightarrow{}  (as  \mequiv{}  as'  upto  x,y.R[x;y]    \mLeftarrow{}{}\mRightarrow{}  bs  \mequiv{}  bs'  upto  x,y.R[x;y]  ))


By

---

Latex:
((BLemma  `equiv\_rel\_self\_functionality`  THENM  BLemma  `permr\_upto\_equiv\_rel`)  THEN  Auto)

---

Home Index