Step
*
1
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)
16. r outl(g a1) < r a1
⊢ gensearch(f;g;x) ∈ B + Top
BY
{ (StrongHypSubst (-2) (-1) THEN Reduce (-1) 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)
16. r x < 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)
16.  r  outl(g  a1)  <  r  a1
\mvdash{}  gensearch(f;g;x)  \mmember{}  B  +  Top
By
Latex:
(StrongHypSubst  (-2)  (-1)  THEN  Reduce  (-1)  THEN  Auto)\mcdot{}
Home
Index