---

Step * 1 of Lemma sqle-append-nil-if-has-value4


1. n : ℤ
2. 0 < n
3. ∀t:ListLike. (t ≤n - 1 t @ [])
4. t : ListLike
5. y : (t)↓
⊢ t ≤n t @ []
BY
{ ((InstLemma `is-list-if-has-value-decomp` [⌜t⌝]⋅ THENA Auto)
   THEN D (-1)
   THEN ExRepD
   THEN Try (Complete ((GenConclAtAddrType ⌜Unit⌝ [2]⋅
                        THEN Auto
                        THEN DVar `v'
                        THEN Reduce 0
                        THEN RepUR ``nil it`` 0
                        THEN Auto
                        THEN Refine_sqle_n
                        THEN Auto)))
   THEN (GenConclAtAddrType ⌜Top × ListLike⌝ [2]⋅ THEN Auto)
   THEN DProdsAndUnions
   THEN Reduce 0
   THEN RepUR ``cons`` 0
   THEN Refine_sqle_n
   THEN Try (Complete (Auto))
   THEN Refine_sqlenSqequaln
   THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  <  n
3.  \mforall{}t:ListLike.  (t  \mleq{}n  -  1  t  @  [])
4.  t  :  ListLike
5.  y  :  (t)\mdownarrow{}
\mvdash{}  t  \mleq{}n  t  @  []


By

---

Latex:
((InstLemma  `is-list-if-has-value-decomp`  [\mkleeneopen{}t\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  (-1)
  THEN  ExRepD
  THEN  Try  (Complete  ((GenConclAtAddrType  \mkleeneopen{}Unit\mkleeneclose{}  [2]\mcdot{}
                                            THEN  Auto
                                            THEN  DVar  `v'
                                            THEN  Reduce  0
                                            THEN  RepUR  ``nil  it``  0
                                            THEN  Auto
                                            THEN  Refine\_sqle\_n
                                            THEN  Auto)))
  THEN  (GenConclAtAddrType  \mkleeneopen{}Top  \mtimes{}  ListLike\mkleeneclose{}  [2]\mcdot{}  THEN  Auto)
  THEN  DProdsAndUnions
  THEN  Reduce  0
  THEN  RepUR  ``cons``  0
  THEN  Refine\_sqle\_n
  THEN  Try  (Complete  (Auto))
  THEN  Refine\_sqlenSqequaln
  THEN  Auto)

---

Home Index