---

Step * 1 1 1 1 2 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')))
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 )||
BY
{ ((RWO "primrec-unroll" 0 THENA Auto)
   THEN (MoveToConcl (-1))
   THEN Reduce 0
   THEN Subst' ((i + 1) - 1) = i ∈ ℤ 0
   THEN RepeatFor 2 (((SplitOnConclITE THENA (Auto THEN DoSubsume THEN Auto)) THEN Try (Complete (Auto))))
   THEN Subst' ((i - 1) + 1) = i ∈ ℤ 0
   THEN TACTIC:(((GenConclAtAddr [1; 2; 1]) THENA Auto)
                THEN TACTIC:(((GenConclAtAddr [2; 2; 1; 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. 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'||

---

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


By

---

Latex:
((RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  (MoveToConcl  (-1))
  THEN  Reduce  0
  THEN  Subst'  ((i  +  1)  -  1)  =  i  0
  THEN  RepeatFor  2  (((SplitOnConclITE  THENA  (Auto  THEN  DoSubsume  THEN  Auto))
                                        THEN  Try  (Complete  (Auto))
                                        ))
  THEN  Subst'  ((i  -  1)  +  1)  =  i  0
  THEN  TACTIC:(((GenConclAtAddr  [1;  2;  1])  THENA  Auto)
                            THEN  TACTIC:(((GenConclAtAddr  [2;  2;  1;  1])  THENA  Auto)
                                                      THEN  D  -2
                                                      THEN  Reduce  0
                                                      THEN  Auto)
                            ))

---

Home Index