---

Step * of Lemma at_AFbar

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ∀n:ℕ. ∀s:AF-spread-law(x,y.R[x;y])-consistent-seq(n).
    ((AFbar() n s) ⇒ (¬{a:T| AF-spread-law(x,y.R[x;y]) n s (inl a)} ))
BY
{ (InstLemma `AFbar_wf` []
   THEN RepeatFor 2 (ParallelLast')
   THEN InstLemma `AF-spread-law_wf` [⌜T⌝;⌜R⌝]⋅
   THEN Auto
   THEN D 0
   THEN Auto
   THEN RepUR ``AFbar`` -2
   THEN RepUR ``AF-spread-law`` -1
   THEN (D -1 THENA Auto)
   THEN (Assert (↑isr(s (n - 1))) ∧ (↑isl(s (n - 1))) BY
               Auto)
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜s (n - 1)⌝⋅ THENA Auto)
   THEN D (-2)⋅
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}n:\mBbbN{}.  \mforall{}s:AF-spread-law(x,y.R[x;y])-consistent-seq(n).
        ((AFbar()  n  s)  {}\mRightarrow{}  (\mneg{}\{a:T|  AF-spread-law(x,y.R[x;y])  n  s  (inl  a)\}  ))


By

---

Latex:
(InstLemma  `AFbar\_wf`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  InstLemma  `AF-spread-law\_wf`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  RepUR  ``AFbar``  -2
  THEN  RepUR  ``AF-spread-law``  -1
  THEN  (D  -1  THENA  Auto)
  THEN  (Assert  (\muparrow{}isr(s  (n  -  1)))  \mwedge{}  (\muparrow{}isl(s  (n  -  1)))  BY
                          Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}s  (n  -  1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  (-2)\mcdot{}
  THEN  Reduce  0
  THEN  Auto)

---

Home Index