---

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

.....assertion..... 
1. [T] : Type
2. X : T
3. R : ℕ ⟶ (T List) ⟶ ℙ
4. p : i:ℕ ⟶ s:(T List) ⟶ (∃s':T List. (s ≤ s' ∧ (R i s')))
⊢ ∃s:ℕ ⟶ (T List). ((∀i:ℕ. (R i (s i))) ∧ (∀i:ℕ. s i ≤ s (i + 1)) ∧ (∀i:ℕ. i < ||s i||))
BY
{ (TACTIC:((InstConcl [⌜λ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 )⌝])⋅
           THENA Auto
           )
   THEN 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:ℕ. (R 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))

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:ℕ
     (λ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)

---

Latex:

---

Latex:
.....assertion..... 
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{}  \mexists{}s:\mBbbN{}  {}\mrightarrow{}  (T  List).  ((\mforall{}i:\mBbbN{}.  (R  i  (s  i)))  \mwedge{}  (\mforall{}i:\mBbbN{}.  s  i  \mleq{}  s  (i  +  1))  \mwedge{}  (\mforall{}i:\mBbbN{}.  i  <  ||s  i||))


By

---

Latex:
(TACTIC:((InstConcl  [\mkleeneopen{}\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  )\mkleeneclose{}])\mcdot{}
                  THENA  Auto
                  )
  THEN  D  0
  )

---

Home Index