---

Step * of Lemma gensearch_wf

∀[A,B:Type]. ∀[r:A ⟶ ℕ]. ∀[f:A ⟶ (B + Top)]. ∀[g:A ⟶ (A + Top)].
  ∀[a:A]. (gensearch(f;g;a) ∈ B + Top) supposing ∀a:A. ((↑isl(g a)) ⇒ r outl(g a) < r a)
BY
{ (Auto
   THEN Assert ⌜∀n:ℕ. ∀a:A.  (((r a) ≤ n) ⇒ (gensearch(f;g;a) ∈ B + Top))⌝⋅
   THEN Try ((InstHyp [⌜r a⌝;⌜a⌝] (-1)⋅ THEN Auto))
   THEN CompleteInductionOnNat
   THEN Auto
   THEN RecUnfold `gensearch` 0
   THEN GenConclAtAddr [2;1]
   THEN D -2
   THEN Reduce 0
   THEN MemCD
   THEN Auto) }

1
1. A : Type
2. B : Type
3. r : A ⟶ ℕ
4. f : A ⟶ (B + Top)
5. g : A ⟶ (A + Top)
6. ∀a:A. ((↑isl(g a)) ⇒ r outl(g a) < r a)
7. a : A
8. n : ℕ
9. ∀n:ℕn. ∀a:A.  (((r a) ≤ n) ⇒ (gensearch(f;g;a) ∈ B + Top))
10. a1 : A@i
11. (r a1) ≤ n
12. y : Top@i
13. (f a1) = (inr y ) ∈ (B + Top)
14. x : A@i
15. (g a1) = (inl x) ∈ (A + Top)
⊢ gensearch(f;g;x) ∈ B + Top

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[r:A  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[f:A  {}\mrightarrow{}  (B  +  Top)].  \mforall{}[g:A  {}\mrightarrow{}  (A  +  Top)].
    \mforall{}[a:A].  (gensearch(f;g;a)  \mmember{}  B  +  Top)  supposing  \mforall{}a:A.  ((\muparrow{}isl(g  a))  {}\mRightarrow{}  r  outl(g  a)  <  r  a)


By

---

Latex:
(Auto
  THEN  Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}a:A.    (((r  a)  \mleq{}  n)  {}\mRightarrow{}  (gensearch(f;g;a)  \mmember{}  B  +  Top))\mkleeneclose{}\mcdot{}
  THEN  Try  ((InstHyp  [\mkleeneopen{}r  a\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto))
  THEN  CompleteInductionOnNat
  THEN  Auto
  THEN  RecUnfold  `gensearch`  0
  THEN  GenConclAtAddr  [2;1]
  THEN  D  -2
  THEN  Reduce  0
  THEN  MemCD
  THEN  Auto)

---

Home Index