---

Step * of Lemma repeat-on-success_wf

∀[A,B:Type].
  (∀[C:Type]. ∀[f:A ⟶ (C?)]. ∀[g:(ℕ × C) ⟶ (A List) ⟶ (A List)].
     ∀[h:(ℕ × C) ⟶ B ⟶ B]. ∀[as:A List]. ∀[b:B].  (repeat-on-success(f;g;h;as;b) ∈ A List × B) 
     supposing ∃m:(A List) ⟶ ℕ
                ∀as:A List. ∀c:C. ∀j:ℕ.
                  ((first-success(f;as) = (inl <j, c>) ∈ (ℕ × C?)) ⇒ m (g <j, c> as) < m as)) supposing 
     (value-type(B) and 
     valueall-type(A))
BY
{ (Auto
   THEN ExRepD
   THEN (Assert ⌜∀n:ℕ. ∀[as:A List]. (m as < n ⇒ (∀[b:B]. (repeat-on-success(f;g;h;as;b) ∈ A List × B)))⌝⋅
   THENM (InstHyp [⌜(m as) + 1⌝;⌜as⌝;⌜b⌝] (-1)⋅ THEN Auto)
   )
   THEN InductionOnNat
   THEN Auto'
   THEN RecUnfold `repeat-on-success` 0
   THEN Reduce 0
   THEN (GenConclTerm ⌜first-success(f;a1)⌝⋅ THENA Auto)
   THEN D -2
   THEN Reduce 0) }

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' = evalall(g x a1) in
  eval b' = h x b1 in
    repeat-on-success(f;g;h;as';b') ∈ A List × B

2
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. y : Unit
20. first-success(f;a1) = (inr y ) ∈ (i:ℕ||a1|| × C?)
⊢ <a1, b1> ∈ A List × B

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    (\mforall{}[C:Type].  \mforall{}[f:A  {}\mrightarrow{}  (C?)].  \mforall{}[g:(\mBbbN{}  \mtimes{}  C)  {}\mrightarrow{}  (A  List)  {}\mrightarrow{}  (A  List)].
          \mforall{}[h:(\mBbbN{}  \mtimes{}  C)  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[as:A  List].  \mforall{}[b:B].    (repeat-on-success(f;g;h;as;b)  \mmember{}  A  List  \mtimes{}  B) 
          supposing  \mexists{}m:(A  List)  {}\mrightarrow{}  \mBbbN{}
                                \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))  supposing 
          (value-type(B)  and 
          valueall-type(A))


By

---

Latex:
(Auto
  THEN  ExRepD
  THEN  (Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}
                                  \mforall{}[as:A  List].  (m  as  <  n  {}\mRightarrow{}  (\mforall{}[b:B].  (repeat-on-success(f;g;h;as;b)  \mmember{}  A  List  \mtimes{}  B)))\mkleeneclose{}
              \mcdot{}
  THENM  (InstHyp  [\mkleeneopen{}(m  as)  +  1\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)
  )
  THEN  InductionOnNat
  THEN  Auto'
  THEN  RecUnfold  `repeat-on-success`  0
  THEN  Reduce  0
  THEN  (GenConclTerm  \mkleeneopen{}first-success(f;a1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0)

---

Home Index