---

Step * 1 of Lemma rel-plus-rel-immediate


1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. x : T
4. y : T
5. n : ℕ+
6. λx,y. ((R x y) ∧ (∀z:T. (¬((R x z) ∧ (R z y)))))^n x y
⊢ R^n x y
BY
{ ((MoveToConcl (-3))
   THEN (MoveToConcl (-2))
   THEN ((NatPlusInd (-1)) THENA Auto)
   THEN (D 0 THENA Auto)
   THEN RecUnfold `rel_exp` 0
   THEN Reduce 0
   THEN Try ((RecUnfold `rel_exp` 0 THEN Reduce 0 THEN Complete (Auto))⋅)
   THEN AutoSplit
   THEN Subst' (n + 1) - 1 ~ n 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [R]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  x  :  T
4.  y  :  T
5.  n  :  \mBbbN{}\msupplus{}
6.  rel\_exp(T;  \mlambda{}x,y.  ((R  x  y)  \mwedge{}  (\mforall{}z:T.  (\mneg{}((R  x  z)  \mwedge{}  (R  z  y)))));  n)  x  y
\mvdash{}  rel\_exp(T;  R;  n)  x  y


By

---

Latex:
((MoveToConcl  (-3))
  THEN  (MoveToConcl  (-2))
  THEN  ((NatPlusInd  (-1))  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  RecUnfold  `rel\_exp`  0
  THEN  Reduce  0
  THEN  Try  ((RecUnfold  `rel\_exp`  0  THEN  Reduce  0  THEN  Complete  (Auto))\mcdot{})
  THEN  AutoSplit
  THEN  Subst'  (n  +  1)  -  1  \msim{}  n  0
  THEN  Auto)

---

Home Index