---

Step * of Lemma non-forking-rel_exp

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (non-forking(T;x,y.R[x;y]) ⇒ (∀n:ℕ. non-forking(T;x,y.x λx,y. R[x;y]^n y)))
BY
{ (InductionOnNat⋅
   THEN RecUnfold `rel_exp` 0
   THEN Reduce 0
   THEN Try (AutoSplit)
   THEN D 0
   THEN Auto
   THEN ExRepD
   THEN Subst ⌜z = z1 ∈ T⌝ (-1)⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (non-forking(T;x,y.R[x;y])  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  non-forking(T;x,y.x  rel\_exp(T;  \mlambda{}x,y.  R[x;y];  n)  y)))


By

---

Latex:
(InductionOnNat\mcdot{}
  THEN  RecUnfold  `rel\_exp`  0
  THEN  Reduce  0
  THEN  Try  (AutoSplit)
  THEN  D  0
  THEN  Auto
  THEN  ExRepD
  THEN  Subst  \mkleeneopen{}z  =  z1\mkleeneclose{}  (-1)\mcdot{}
  THEN  Auto)

---

Home Index