Step * 2 of Lemma repeat-on-success_wf


1. Type
2. Type
3. valueall-type(A)
4. value-type(B)
5. Type
6. A ⟶ (C?)
7. (ℕ × C) ⟶ (A List) ⟶ (A List)
8. (A List) ⟶ ℕ
9. ∀as:A List. ∀c:C. ∀j:ℕ.  ((first-success(f;as) (inl <j, c>) ∈ (ℕ × C?))  (g <j, c> as) < as)
10. (ℕ × C) ⟶ B ⟶ B
11. as List
12. B
13. : ℤ
14. 0 < n
15. ∀[as:A List]. (m as <  (∀[b:B]. (repeat-on-success(f;g;h;as;b) ∈ List × B)))
16. a1 List
17. a1 < n
18. b1 B
19. Unit
20. first-success(f;a1) (inr ) ∈ (i:ℕ||a1|| × C?)
⊢ <a1, b1> ∈ List × B
BY
Auto }


Latex:


Latex:

1.  A  :  Type
2.  B  :  Type
3.  valueall-type(A)
4.  value-type(B)
5.  C  :  Type
6.  f  :  A  {}\mrightarrow{}  (C?)
7.  g  :  (\mBbbN{}  \mtimes{}  C)  {}\mrightarrow{}  (A  List)  {}\mrightarrow{}  (A  List)
8.  m  :  (A  List)  {}\mrightarrow{}  \mBbbN{}
9.  \mforall{}as:A  List.  \mforall{}c:C.  \mforall{}j:\mBbbN{}.    ((first-success(f;as)  =  (inl  <j,  c>))  {}\mRightarrow{}  m  (g  <j,  c>  as)  <  m  as)
10.  h  :  (\mBbbN{}  \mtimes{}  C)  {}\mrightarrow{}  B  {}\mrightarrow{}  B
11.  as  :  A  List
12.  b  :  B
13.  n  :  \mBbbZ{}
14.  0  <  n
15.  \mforall{}[as:A  List].  (m  as  <  n  -  1  {}\mRightarrow{}  (\mforall{}[b:B].  (repeat-on-success(f;g;h;as;b)  \mmember{}  A  List  \mtimes{}  B)))
16.  a1  :  A  List
17.  m  a1  <  n
18.  b1  :  B
19.  y  :  Unit
20.  first-success(f;a1)  =  (inr  y  )
\mvdash{}  <a1,  b1>  \mmember{}  A  List  \mtimes{}  B


By


Latex:
Auto




Home Index