---

Step * of Lemma AF-path-barred

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (AFx,y:T.R[x;y] ⇒ (∀alpha:{f:ℕ ⟶ (T?)| ∀x:ℕ. (AF-spread-law(x,y.R[x;y]) x f (f x))} . (↓∃m:ℕ. (AFbar() m alpha))))
BY
{ (InstLemma `AF-spread-law_wf` []
   THEN RepeatFor 2 (ParallelLast')
   THEN Auto
   THEN D -1
   THEN RepUR ``AFbar`` 0
   THEN (Decide ⌜↑isr(alpha 0)⌝⋅ THENA Auto)
   THEN Try ((D 0 THEN With ⌜1⌝ (D 0)⋅ THEN Complete (Auto)))
   THEN (Assert T BY
               (UseWitness ⌜outl(alpha 0)⌝⋅ THEN EAuto 2))
   THEN RenameVar `t' (-1)
   THEN PromoteHyp (-1) 2
   THEN Thin (-1)
   THEN Thin (-4)
   THEN RepUR ``AF-spread-law`` -1
   THEN (With ⌜λn.case alpha n of inl(x) => x | inr(x) => t⌝ (D 4)⋅ THENA Auto)
   THEN Reduce (-1)
   THEN D -1
   THEN ExRepD) }

1
1. T : Type
2. t : T
3. R : T ⟶ T ⟶ ℙ
4. alpha : ℕ ⟶ (T?)@i
5. ∀x:ℕ. ((↑isl(alpha x)) ⇒ (∀i:ℕx. ((↑isl(alpha i)) ∧ (¬R[outl(alpha i);outl(alpha x)]))))
6. i : ℕ@i
7. j : ℕ@i
8. i < j
9. R[case alpha i of inl(x) => x | inr(x) => t;case alpha j of inl(x) => x | inr(x) => t]
⊢ ↓∃m:ℕ. (0 < m ∧ (↑isr(alpha (m - 1))))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (AFx,y:T.R[x;y]
    {}\mRightarrow{}  (\mforall{}alpha:\{f:\mBbbN{}  {}\mrightarrow{}  (T?)|  \mforall{}x:\mBbbN{}.  (AF-spread-law(x,y.R[x;y])  x  f  (f  x))\} 
                (\mdownarrow{}\mexists{}m:\mBbbN{}.  (AFbar()  m  alpha))))


By

---

Latex:
(InstLemma  `AF-spread-law\_wf`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  Auto
  THEN  D  -1
  THEN  RepUR  ``AFbar``  0
  THEN  (Decide  \mkleeneopen{}\muparrow{}isr(alpha  0)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  ((D  0  THEN  With  \mkleeneopen{}1\mkleeneclose{}  (D  0)\mcdot{}  THEN  Complete  (Auto)))
  THEN  (Assert  T  BY
                          (UseWitness  \mkleeneopen{}outl(alpha  0)\mkleeneclose{}\mcdot{}  THEN  EAuto  2))
  THEN  RenameVar  `t'  (-1)
  THEN  PromoteHyp  (-1)  2
  THEN  Thin  (-1)
  THEN  Thin  (-4)
  THEN  RepUR  ``AF-spread-law``  -1
  THEN  (With  \mkleeneopen{}\mlambda{}n.case  alpha  n  of  inl(x)  =>  x  |  inr(x)  =>  t\mkleeneclose{}  (D  4)\mcdot{}  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  D  -1
  THEN  ExRepD)

---

Home Index