---

Step * of Lemma permr_upto_transitivity

∀T:Type. ∀R:T ⟶ T ⟶ ℙ.
  (EquivRel(T;x,y.R[x;y])
  ⇒ (∀as,bs,cs:T List.  (as ≡ bs upto x,y.R[x;y]  ⇒ bs ≡ cs upto x,y.R[x;y]  ⇒ as ≡ cs upto x,y.R[x;y] )))
BY
{ ((UnivCD THEN Auto)
   THEN OnCls [-2; -1; 0] UnfoldTopAb
   THEN RepUnfolds ``equiv_rel refl sym trans`` 3
   THEN ExistHD 3) }

1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. ∀a:T. R[a;a]
4. ∀a,b:T.  (R[a;b] ⇒ R[b;a])
5. ∀a,b,c:T.  (R[a;b] ⇒ R[b;c] ⇒ R[a;c])
6. as : T List
7. bs : T List
8. cs : T List
9. (||as|| = ||bs|| ∈ ℤ) c∧ (∃p:Sym(||as||). ∀i:ℕ||as||. R[as[p.f i];bs[i]])
10. (||bs|| = ||cs|| ∈ ℤ) c∧ (∃p:Sym(||bs||). ∀i:ℕ||bs||. R[bs[p.f i];cs[i]])
⊢ (||as|| = ||cs|| ∈ ℤ) c∧ (∃p:Sym(||as||). ∀i:ℕ||as||. R[as[p.f i];cs[i]])

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.
    (EquivRel(T;x,y.R[x;y])
    {}\mRightarrow{}  (\mforall{}as,bs,cs:T  List.
                (as  \mequiv{}  bs  upto  x,y.R[x;y]    {}\mRightarrow{}  bs  \mequiv{}  cs  upto  x,y.R[x;y]    {}\mRightarrow{}  as  \mequiv{}  cs  upto  x,y.R[x;y]  )))


By

---

Latex:
((UnivCD  THEN  Auto)
  THEN  OnCls  [-2;  -1;  0]  UnfoldTopAb
  THEN  RepUnfolds  ``equiv\_rel  refl  sym  trans``  3
  THEN  ExistHD  3)

---

Home Index