---

Step * 1 1 1 1 2 2 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')))
⊢ ∀i:ℕ. i < ||(λn.primrec(n + 1;[];λi,s. if i <z ||fst((p i s))|| then fst((p i s)) else fst((p i (s @ [X]))) fi )) i||
BY
{ ((TACTIC:InductionOnNat THENA Auto) THEN Reduce 0 THEN Auto') }

1
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 : ℤ
⊢ 0 < ||if 0 <z ||fst((p 0 []))|| then fst((p 0 [])) else fst((p 0 [X])) fi ||

2
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. i - 1 < ||(λn.primrec(n + 1;[];λi,s. if i <z ||fst((p i s))|| then fst((p i s)) else fst((p i (s @ [X]))) fi )) (i - \000C1)||
⊢ i < ||primrec(i + 1;[];λi,s. if i <z ||fst((p i s))|| then fst((p i s)) else fst((p i (s @ [X]))) fi )||

---

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')))
\mvdash{}  \mforall{}i:\mBbbN{}
        i  <  ||(\mlambda{}n.primrec(n  +  1;[];\mlambda{}i,s.  if  i  <z  ||fst((p  i  s))||
                                                                        then  fst((p  i  s))
                                                                        else  fst((p  i  (s  @  [X])))
                                                                        fi  )) 
                    i||


By

---

Latex:
((TACTIC:InductionOnNat  THENA  Auto)  THEN  Reduce  0  THEN  Auto')

---

Home Index