---

Step * 1 1 1 1 2 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')))
5. i : ℤ
⊢ 0 < ||if 0 <z ||fst((p 0 []))|| then fst((p 0 [])) else fst((p 0 [X])) fi ||
BY
{ ((SplitOnConclITE THENA Auto)
   THEN Try (Complete (Auto))
   THEN ((GenConclAtAddr [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. ||fst((p 0 []))|| ≤ 0
7. s' : T List
8. v2 : [X] ≤ s'
9. v3 : R 0 s'
10. (p 0 [X]) = <s', v2, v3> ∈ (∃s':T List. ([X] ≤ s' ∧ (R 0 s')))
⊢ 0 < ||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{}
\mvdash{}  0  <  ||if  0  <z  ||fst((p  0  []))||  then  fst((p  0  []))  else  fst((p  0  [X]))  fi  ||


By

---

Latex:
((SplitOnConclITE  THENA  Auto)
  THEN  Try  (Complete  (Auto))
  THEN  ((GenConclAtAddr  [2;  1;  1])  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto)

---

Home Index