---

Step * 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. ∀i:ℕ||as||. (R as[pa.f i] bs[i])
12. ||bs|| = ||cs|| ∈ ℤ
13. pb : Sym(||bs||)
14. ∀i:ℕ||bs||. (R bs[pb.f i] cs[i])
15. ||as|| = ||cs|| ∈ ℤ
16. i : ℕ||as||
⊢ R as[pa.f (pb.f i)] cs[i]
BY
{ With i (D 14) THENM With pb.f i (D 11) 
THENA Auto }

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|| ∈ ℤ
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]

---

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.  \mforall{}i:\mBbbN{}||as||.  (R  as[pa.f  i]  bs[i])
12.  ||bs||  =  ||cs||
13.  pb  :  Sym(||bs||)
14.  \mforall{}i:\mBbbN{}||bs||.  (R  bs[pb.f  i]  cs[i])
15.  ||as||  =  ||cs||
16.  i  :  \mBbbN{}||as||
\mvdash{}  R  as[pa.f  (pb.f  i)]  cs[i]


By

---

Latex:
With  i  (D  14)  THENM  With  pb.f  i  (D  11) 
THENA  Auto

---

Home Index