---

Step * 1 1 1 1 1 1 of Lemma permr_upto_transitivity


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|| ∈ ℤ
10. pa : Sym(||as||)
11. ||bs|| = ||cs|| ∈ ℤ
12. pb : Sym(||bs||)
13. ||as|| = ||cs|| ∈ ℤ
14. i : ℕ||as||
15. R bs[pb.f i] cs[i]
16. R as[pa.f (pb.f i)] bs[pb.f i]
⊢ R as[pa.f (pb.f i)] cs[i]
BY
{ FHyp 5 [15;16] THEN Auto' }

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}a:T.  (R  a  a)
4.  \mforall{}a,b:T.    ((R  a  b)  {}\mRightarrow{}  (R  b  a))
5.  \mforall{}a,b,c:T.    ((R  a  b)  {}\mRightarrow{}  (R  b  c)  {}\mRightarrow{}  (R  a  c))
6.  as  :  T  List
7.  bs  :  T  List
8.  cs  :  T  List
9.  ||as||  =  ||bs||
10.  pa  :  Sym(||as||)
11.  ||bs||  =  ||cs||
12.  pb  :  Sym(||bs||)
13.  ||as||  =  ||cs||
14.  i  :  \mBbbN{}||as||
15.  R  bs[pb.f  i]  cs[i]
16.  R  as[pa.f  (pb.f  i)]  bs[pb.f  i]
\mvdash{}  R  as[pa.f  (pb.f  i)]  cs[i]


By

---

Latex:
FHyp  5  [15;16]  THEN  Auto'

---

Home Index