---

Step * 1 1 1 1 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:ℕ
     (λ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 ≤
      (λ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 + 1))
∧ (∀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||\000C)
BY
{ D 0 }

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')))
⊢ ∀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 ≤
     (λ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 + 1)

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')))
⊢ ∀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||

---

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{}
          (\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  \mleq{}  (\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  +  1))
\mwedge{}  (\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:
D  0

---

Home Index