---

Step * of Lemma transitive-closure-symmetric

∀[A:Type]. ∀[R:A ⟶ A ⟶ ℙ].  (Sym(A;x,y.R x y) ⇒ Sym(A;x,y.x TC(R) y))
BY
{ (TACTIC:Auto
   THEN ParallelLast
   THEN RenameVar `s' (-1)
   THEN Auto
   THEN ParallelLast
   THEN RepUR ``transitive-closure`` -1
   THEN RepUR ``transitive-closure`` 0
   THEN RenameVar `L' (-1)) }

1
1. [A] : Type
2. [R] : A ⟶ A ⟶ ℙ
3. s : ∀a,b:A.  ((R a b) ⇒ (R b a))
4. a : A
5. b : A
6. L : {L:(a:A × b:A × (R a b)) List| rel_path(A;L;a;b) ∧ 0 < ||L||} 
⊢ {L:(a:A × b:A × (R a b)) List| rel_path(A;L;b;a) ∧ 0 < ||L||} 

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].    (Sym(A;x,y.R  x  y)  {}\mRightarrow{}  Sym(A;x,y.x  TC(R)  y))


By

---

Latex:
(TACTIC:Auto
  THEN  ParallelLast
  THEN  RenameVar  `s'  (-1)
  THEN  Auto
  THEN  ParallelLast
  THEN  RepUR  ``transitive-closure``  -1
  THEN  RepUR  ``transitive-closure``  0
  THEN  RenameVar  `L'  (-1))

---

Home Index