---

Step * of Lemma list-decomp-nat

∀[T:Type]. ∀L:T List. ∀i:ℕ||L|| + 1.  ∃K,J:T List. ((L = (K @ J) ∈ (T List)) ∧ (||K|| = i ∈ ℤ))
BY
{ (InductionOnList
   THEN Reduce 0
   THEN Auto
   THEN Try (Complete ((IntSegCases (-1) THEN InstConcl [⌜[]⌝;⌜[]⌝]⋅ THEN Auto)))
   THEN (Decide i = 0 ∈ ℤ THENA Auto)
   THEN Try (Complete ((InstConcl [⌜[]⌝;⌜[u / v]⌝]⋅ THEN Reduce 0 THEN Auto)))
   THEN (InstHyp [⌜i - 1⌝] (-3)⋅ THENA Auto)
   THEN ExRepD
   THEN InstConcl [⌜[u / K]⌝;⌜J⌝]⋅
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mforall{}i:\mBbbN{}||L||  +  1.    \mexists{}K,J:T  List.  ((L  =  (K  @  J))  \mwedge{}  (||K||  =  i))


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  (Complete  ((IntSegCases  (-1)  THEN  InstConcl  [\mkleeneopen{}[]\mkleeneclose{};\mkleeneopen{}[]\mkleeneclose{}]\mcdot{}  THEN  Auto)))
  THEN  (Decide  i  =  0  THENA  Auto)
  THEN  Try  (Complete  ((InstConcl  [\mkleeneopen{}[]\mkleeneclose{};\mkleeneopen{}[u  /  v]\mkleeneclose{}]\mcdot{}  THEN  Reduce  0  THEN  Auto)))
  THEN  (InstHyp  [\mkleeneopen{}i  -  1\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  InstConcl  [\mkleeneopen{}[u  /  K]\mkleeneclose{};\mkleeneopen{}J\mkleeneclose{}]\mcdot{}
  THEN  Reduce  0
  THEN  Auto)

---

Home Index