---

Step * of Lemma transitive-loop

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (Trans(T;x,y.R[x;y])
  ⇒ (∀L:T List. ((∀i:ℕ||L|| - 1. R[L[i];L[i + 1]]) ⇒ R[last(L);hd(L)] supposing ¬↑null(L) ⇒ (∀a∈L.(∀b∈L.R[a;b])))))
BY
{ (Auto THEN RWW "l_all_iff" 0 THEN Auto THEN (Assert ¬↑null(L) BY (DVar `L'  THEN Reduce 0 THEN Auto))) }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. Trans(T;x,y.R[x;y])
4. L : T List
5. ∀i:ℕ||L|| - 1. R[L[i];L[i + 1]]
6. R[last(L);hd(L)] supposing ¬↑null(L)
7. a : T
8. (a ∈ L)
9. b : T
10. (b ∈ L)
11. ¬↑null(L)
⊢ R[a;b]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (Trans(T;x,y.R[x;y])
    {}\mRightarrow{}  (\mforall{}L:T  List
                ((\mforall{}i:\mBbbN{}||L||  -  1.  R[L[i];L[i  +  1]])
                {}\mRightarrow{}  R[last(L);hd(L)]  supposing  \mneg{}\muparrow{}null(L)
                {}\mRightarrow{}  (\mforall{}a\mmember{}L.(\mforall{}b\mmember{}L.R[a;b])))))


By

---

Latex:
(Auto
  THEN  RWW  "l\_all\_iff"  0
  THEN  Auto
  THEN  (Assert  \mneg{}\muparrow{}null(L)  BY
                          (DVar  `L'    THEN  Reduce  0  THEN  Auto)))

---

Home Index