---

Step * 1 of Lemma gensearch_wf


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
BY
{ TACTIC:(InstHyp [⌜a1⌝] 6⋅ THENA 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)
16. r outl(g a1) < r a1
⊢ gensearch(f;g;x) ∈ B + Top

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  r  :  A  {}\mrightarrow{}  \mBbbN{}
4.  f  :  A  {}\mrightarrow{}  (B  +  Top)
5.  g  :  A  {}\mrightarrow{}  (A  +  Top)
6.  \mforall{}a:A.  ((\muparrow{}isl(g  a))  {}\mRightarrow{}  r  outl(g  a)  <  r  a)
7.  a  :  A
8.  n  :  \mBbbN{}
9.  \mforall{}n:\mBbbN{}n.  \mforall{}a:A.    (((r  a)  \mleq{}  n)  {}\mRightarrow{}  (gensearch(f;g;a)  \mmember{}  B  +  Top))
10.  a1  :  A@i
11.  (r  a1)  \mleq{}  n
12.  y  :  Top@i
13.  (f  a1)  =  (inr  y  )
14.  x  :  A@i
15.  (g  a1)  =  (inl  x)
\mvdash{}  gensearch(f;g;x)  \mmember{}  B  +  Top


By

---

Latex:
TACTIC:(InstHyp  [\mkleeneopen{}a1\mkleeneclose{}]  6\mcdot{}  THENA  Auto)

---

Home Index