---

Step * of Lemma mu-dec-property

∀[A:Type]. ∀[P:A ⟶ ℕ ⟶ ℙ].
  ∀d:a:A ⟶ k:ℕ ⟶ Dec(P[a;k]). ∀a:A.  ((↓∃k:ℕ. P[a;k]) ⇒ {P[a;mu-dec(d;a)] ∧ (∀i:ℕmu-dec(d;a). (¬P[a;i]))})
BY
{ (InstLemma `mu-dec_wf` []
   THEN RepeatFor 5 (ParallelLast')
   THEN Auto
   THEN (Assert ⌜Dec(P[a;mu-dec(d;a)])⌝⋅ THENA (UseWitness ⌜d[a;mu-dec(d;a)]⌝⋅ THEN Auto))
   THEN Unfold `guard` 0
   THEN D -3
   THEN (Unhide THENA Auto)
   THEN Thin (-1)
   THEN Auto
   THEN All (RepUR ``decidable or mu-dec``)
   THEN (InstLemma `mu-property` [⌜λk.isl(d a k)⌝]⋅ THENA (Auto THEN Reduce 0))
   THEN All (Fold `mu-dec`)
   THEN Reduce (-1)
   THEN (Try (OnMaybeHyp 5 (\h. (ParallelOp h THEN GenConclAtAddr [1;1] THEN D -2 THEN Reduce 0 THEN Complete (Auto))))
         THEN D -1
         THEN Try ((InstHyp [⌜i⌝] (-1)⋅ THENA (Auto THEN SubsumeC ⌜ℕ⌝⋅ THEN Auto))⋅))⋅) }

1
1. A : Type
2. P : A ⟶ ℕ ⟶ ℙ
3. d : a:A ⟶ k:ℕ ⟶ (P[a;k] + (¬P[a;k]))@i
4. a : A@i
5. ∃k:ℕ. P[a;k]@i
6. mu-dec(d;a) ∈ ℕ
7. ↑isl(d a mu-dec(d;a))
8. ∀[i:ℕ]. ¬↑isl(d a i) supposing i < mu-dec(d;a)
⊢ P[a;mu-dec(d;a)]

2
1. A : Type
2. P : A ⟶ ℕ ⟶ ℙ
3. d : a:A ⟶ k:ℕ ⟶ (P[a;k] + (¬P[a;k]))@i
4. a : A@i
5. ∃k:ℕ. P[a;k]@i
6. mu-dec(d;a) ∈ ℕ
7. P[a;mu-dec(d;a)]
8. i : ℕmu-dec(d;a)@i
9. ↑isl(d a mu-dec(d;a))
10. ∀[i:ℕ]. ¬↑isl(d a i) supposing i < mu-dec(d;a)
11. ¬↑isl(d a i)
⊢ ¬P[a;i]

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}d:a:A  {}\mrightarrow{}  k:\mBbbN{}  {}\mrightarrow{}  Dec(P[a;k]).  \mforall{}a:A.
        ((\mdownarrow{}\mexists{}k:\mBbbN{}.  P[a;k])  {}\mRightarrow{}  \{P[a;mu-dec(d;a)]  \mwedge{}  (\mforall{}i:\mBbbN{}mu-dec(d;a).  (\mneg{}P[a;i]))\})


By

---

Latex:
(InstLemma  `mu-dec\_wf`  []
  THEN  RepeatFor  5  (ParallelLast')
  THEN  Auto
  THEN  (Assert  \mkleeneopen{}Dec(P[a;mu-dec(d;a)])\mkleeneclose{}\mcdot{}  THENA  (UseWitness  \mkleeneopen{}d[a;mu-dec(d;a)]\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  Unfold  `guard`  0
  THEN  D  -3
  THEN  (Unhide  THENA  Auto)
  THEN  Thin  (-1)
  THEN  Auto
  THEN  All  (RepUR  ``decidable  or  mu-dec``)
  THEN  (InstLemma  `mu-property`  [\mkleeneopen{}\mlambda{}k.isl(d  a  k)\mkleeneclose{}]\mcdot{}  THENA  (Auto  THEN  Reduce  0))
  THEN  All  (Fold  `mu-dec`)
  THEN  Reduce  (-1)
  THEN  (Try  (OnMaybeHyp  5  (\mbackslash{}h.  (ParallelOp  h
                                                              THEN  GenConclAtAddr  [1;1]
                                                              THEN  D  -2
                                                              THEN  Reduce  0
                                                              THEN  Complete  (Auto))))
              THEN  D  -1
              THEN  Try  ((InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  (-1)\mcdot{}  THENA  (Auto  THEN  SubsumeC  \mkleeneopen{}\mBbbN{}\mkleeneclose{}\mcdot{}  THEN  Auto))\mcdot{}))\mcdot{})

---

Home Index