---

Step * 1 1 1 1 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')))
⊢ ∀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)
BY
{ (Reduce 0
   THEN Auto
   THEN ((RW (AddrC [3] (LemmaC `primrec-unroll`)) 0) THENA Auto)
   THEN Reduce 0
   THEN Subst' (((i + 1) + 1) - 1) = (i + 1) ∈ ℤ 0
   THEN RepeatFor 2 (((SplitOnConclITE THENA (Auto THEN DoSubsume THEN Auto)) THEN Auto))
   THEN TACTIC:(((GenConclAtAddr [2]) THENA Auto)
                THEN ((GenConclAtAddr [3; 1]) THENA Auto)
                THEN D -2
                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 : ℕ
6. 1 ≤ ((i + 1) + 1)
7. ||fst((p (i + 1) primrec(i + 1;[];λi,s. if i <z ||fst((p i s))|| then fst((p i s)) else fst((p i (s @ [X]))) fi )))||\000C 
   ≤ (i + 1)
8. v : T List
9. primrec(i + 1;[];λi,s. if i <z ||fst((p i s))|| then fst((p i s)) else fst((p i (s @ [X]))) fi ) = v ∈ (T List)
10. s' : T List
11. v3 : v @ [X] ≤ s'
12. v4 : R (i + 1) s'
13. (p (i + 1) (v @ [X])) = <s', v3, v4> ∈ (∃s':T List. (v @ [X] ≤ s' ∧ (R (i + 1) s')))
⊢ v ≤ s'

---

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)


By

---

Latex:
(Reduce  0
  THEN  Auto
  THEN  ((RW  (AddrC  [3]  (LemmaC  `primrec-unroll`))  0)  THENA  Auto)
  THEN  Reduce  0
  THEN  Subst'  (((i  +  1)  +  1)  -  1)  =  (i  +  1)  0
  THEN  RepeatFor  2  (((SplitOnConclITE  THENA  (Auto  THEN  DoSubsume  THEN  Auto))  THEN  Auto))
  THEN  TACTIC:(((GenConclAtAddr  [2])  THENA  Auto)
                            THEN  ((GenConclAtAddr  [3;  1])  THENA  Auto)
                            THEN  D  -2
                            THEN  Reduce  0
                            THEN  Auto))

---

Home Index