---

Step * 1 1 1 1 2 2 2 1 of Lemma generic-non-empty


1. T : Type
2. X : T
3. R : ℕ ⟶ (T List) ⟶ ℙ
4. p : i:ℕ ⟶ s:(T List) ⟶ (∃s':T List. (s ≤ s' ∧ (R i s')))
5. i : ℤ
6. 0 < i
7. 1 ≤ (i + 1)
8. ||fst((p i primrec(i;[];λi,s. if i <z ||fst((p i s))|| then fst((p i s)) else fst((p i (s @ [X]))) fi )))|| ≤ i
9. v : T List
10. primrec(i;[];λi,s. if i <z ||fst((p i s))|| then fst((p i s)) else fst((p i (s @ [X]))) fi ) = v ∈ (T List)
11. s' : T List
12. v3 : v @ [X] ≤ s'
13. v4 : R i s'
14. (p i (v @ [X])) = <s', v3, v4> ∈ (∃s':T List. (v @ [X] ≤ s' ∧ (R i s')))
15. i - 1 < ||v||
⊢ i < ||s'||
BY
{ (((FLemma `iseg_length` [(-4)]) THENA Auto)
   THEN ((RWO "length_append" (-1)) THENA Auto)
   THEN (Reduce (-1))
   THEN Auto')⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  X  :  T
3.  R  :  \mBbbN{}  {}\mrightarrow{}  (T  List)  {}\mrightarrow{}  \mBbbP{}
4.  p  :  i:\mBbbN{}  {}\mrightarrow{}  s:(T  List)  {}\mrightarrow{}  (\mexists{}s':T  List.  (s  \mleq{}  s'  \mwedge{}  (R  i  s')))
5.  i  :  \mBbbZ{}
6.  0  <  i
7.  1  \mleq{}  (i  +  1)
8.  ||fst((p  i 
                    primrec(i;[];\mlambda{}i,s.  if  i  <z  ||fst((p  i  s))||
                                                        then  fst((p  i  s))
                                                        else  fst((p  i  (s  @  [X])))
                                                        fi  )))||  \mleq{}  i
9.  v  :  T  List
10.  primrec(i;[];\mlambda{}i,s.  if  i  <z  ||fst((p  i  s))||  then  fst((p  i  s))  else  fst((p  i  (s  @  [X])))  fi  )  =  v
11.  s'  :  T  List
12.  v3  :  v  @  [X]  \mleq{}  s'
13.  v4  :  R  i  s'
14.  (p  i  (v  @  [X]))  =  <s',  v3,  v4>
15.  i  -  1  <  ||v||
\mvdash{}  i  <  ||s'||


By

---

Latex:
(((FLemma  `iseg\_length`  [(-4)])  THENA  Auto)
  THEN  ((RWO  "length\_append"  (-1))  THENA  Auto)
  THEN  (Reduce  (-1))
  THEN  Auto')\mcdot{}

---

Home Index