---

Step * 1 of Lemma repeat-on-success_wf


1. A : Type
2. B : Type
3. valueall-type(A)
4. value-type(B)
5. C : Type
6. f : A ⟶ (C?)
7. g : (ℕ × C) ⟶ (A List) ⟶ (A List)
8. m : (A List) ⟶ ℕ
9. ∀as:A List. ∀c:C. ∀j:ℕ.  ((first-success(f;as) = (inl <j, c>) ∈ (ℕ × C?)) ⇒ m (g <j, c> as) < m as)
10. h : (ℕ × C) ⟶ B ⟶ B
11. as : A List
12. b : B
13. n : ℤ
14. 0 < n
15. ∀[as:A List]. (m as < n - 1 ⇒ (∀[b:B]. (repeat-on-success(f;g;h;as;b) ∈ A List × B)))
16. a1 : A List
17. m a1 < n
18. b1 : B
19. x : i:ℕ||a1|| × C
20. first-success(f;a1) = (inl x) ∈ (i:ℕ||a1|| × C?)
⊢ eval as' = evalall(g x a1) in
  eval b' = h x b1 in
    repeat-on-success(f;g;h;as';b') ∈ A List × B
BY
{ ((RWO "evalall-reduce" 0 THENA Auto) THEN Try ((BLemma `list-valueall-type` THEN Auto))) }

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

---

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.  x  :  i:\mBbbN{}||a1||  \mtimes{}  C
20.  first-success(f;a1)  =  (inl  x)
\mvdash{}  eval  as'  =  evalall(g  x  a1)  in
    eval  b'  =  h  x  b1  in
        repeat-on-success(f;g;h;as';b')  \mmember{}  A  List  \mtimes{}  B


By

---

Latex:
((RWO  "evalall-reduce"  0  THENA  Auto)  THEN  Try  ((BLemma  `list-valueall-type`  THEN  Auto)))

---

Home Index