---

Step * of Lemma first-m-not-reg-property

∀[X:Type]
  ∀d:metric(X). ∀k:ℕ. ∀s:ℕk ⟶ X.
    ((first-m-not-reg(d;s;k) = 0 ∈ ℤ ⇐⇒ ∀n:ℕk. m-not-reg(d;s;n) = ff)
    ∧ let i = first-m-not-reg(d;s;k) - 1 in
          (∀n:ℕi. m-not-reg(d;s;n) = ff) ∧ m-not-reg(d;s;i) = tt 
      supposing 0 < first-m-not-reg(d;s;k))
BY
{ (RepeatFor 4 ((D 0 THENA Auto))
   THEN Unfold `first-m-not-reg` 0
   THEN (InstLemma `search_property` [⌜k⌝;⌜λn.m-not-reg(d;s;n)⌝]⋅ THENA Auto)
   THEN Reduce -1
   THEN ParallelLast
   THEN All (Fold `first-m-not-reg`)) }

1
1. [X] : Type
2. d : metric(X)
3. k : ℕ
4. s : ℕk ⟶ X
5. (↑m-not-reg(d;s;first-m-not-reg(d;s;k) - 1)) ∧ (∀j:ℕk. ¬↑m-not-reg(d;s;j) supposing j < first-m-not-reg(d;s;k) - 1) 
   supposing 0 < first-m-not-reg(d;s;k)
6. ∃i:ℕk. (↑m-not-reg(d;s;i)) ⇐⇒ 0 < first-m-not-reg(d;s;k)
⊢ first-m-not-reg(d;s;k) = 0 ∈ ℤ ⇐⇒ ∀n:ℕk. m-not-reg(d;s;n) = ff

2
1. [X] : Type
2. d : metric(X)
3. k : ℕ
4. s : ℕk ⟶ X
5. ∃i:ℕk. (↑m-not-reg(d;s;i)) ⇐⇒ 0 < first-m-not-reg(d;s;k)
6. (↑m-not-reg(d;s;first-m-not-reg(d;s;k) - 1)) ∧ (∀j:ℕk. ¬↑m-not-reg(d;s;j) supposing j < first-m-not-reg(d;s;k) - 1) 
   supposing 0 < first-m-not-reg(d;s;k)
⊢ let i = first-m-not-reg(d;s;k) - 1 in
      (∀n:ℕi. m-not-reg(d;s;n) = ff) ∧ m-not-reg(d;s;i) = tt 
  supposing 0 < first-m-not-reg(d;s;k)

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}d:metric(X).  \mforall{}k:\mBbbN{}.  \mforall{}s:\mBbbN{}k  {}\mrightarrow{}  X.
        ((first-m-not-reg(d;s;k)  =  0  \mLeftarrow{}{}\mRightarrow{}  \mforall{}n:\mBbbN{}k.  m-not-reg(d;s;n)  =  ff)
        \mwedge{}  let  i  =  first-m-not-reg(d;s;k)  -  1  in
                    (\mforall{}n:\mBbbN{}i.  m-not-reg(d;s;n)  =  ff)  \mwedge{}  m-not-reg(d;s;i)  =  tt 
            supposing  0  <  first-m-not-reg(d;s;k))


By

---

Latex:
(RepeatFor  4  ((D  0  THENA  Auto))
  THEN  Unfold  `first-m-not-reg`  0
  THEN  (InstLemma  `search\_property`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}\mlambda{}n.m-not-reg(d;s;n)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Reduce  -1
  THEN  ParallelLast
  THEN  All  (Fold  `first-m-not-reg`))

---

Home Index