---

Step * of Lemma guarded_permutation_transitivity

∀[T:Type]. ∀[P:L:(T List) ⟶ ℕ||L|| - 1 ⟶ ℙ].  Trans(T List)(_1 guarded_permutation(T;P) _2)
BY
{ (((((Auto THEN Unfolds ``guarded_permutation trans`` 0) THEN Reduce 0) THEN Auto)
    THEN Using [`y',b] (BackThruLemma `rel_star_transitivity`)
    )
   THEN Auto
   ) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:L:(T  List)  {}\mrightarrow{}  \mBbbN{}||L||  -  1  {}\mrightarrow{}  \mBbbP{}].    Trans(T  List)($_{1}$  guarded\_per\000Cmutation(T;P)  $_{2}$)


By

---

Latex:
(((((Auto  THEN  Unfolds  ``guarded\_permutation  trans``  0)  THEN  Reduce  0)  THEN  Auto)
    THEN  Using  [`y',b]  (BackThruLemma  `rel\_star\_transitivity`)
    )
  THEN  Auto
  )

---

Home Index