---

Step * 1 1 of Lemma first-member-iff


1. T : Type
2. L : T List
3. P : T ⟶ 𝔹
4. x : T
5. i : ℕ||L||
6. x = L[i] ∈ T
7. ↑(P x)
8. ∀j:ℕi. (¬↑(P L[j]))
⊢ L = (firstn(i;L) @ [x / nth_tl(i + 1;L)]) ∈ (T List)
BY
{ (((HypSubst (-3) 0 THENA Auto) THEN (Subst ⌜i + 1 ~ 1 + i⌝ 0⋅ THENA Auto))
   THEN (InstLemma `nth_tl_decomp_eq` [⌜T⌝;⌜i⌝;⌜L⌝]⋅ THENA Auto)
   THEN (RevHypSubst (-1) 0 THENA Auto)
   THEN RWO "append_firstn_lastn_sq<" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
3.  P  :  T  {}\mrightarrow{}  \mBbbB{}
4.  x  :  T
5.  i  :  \mBbbN{}||L||
6.  x  =  L[i]
7.  \muparrow{}(P  x)
8.  \mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}(P  L[j]))
\mvdash{}  L  =  (firstn(i;L)  @  [x  /  nth\_tl(i  +  1;L)])


By

---

Latex:
(((HypSubst  (-3)  0  THENA  Auto)  THEN  (Subst  \mkleeneopen{}i  +  1  \msim{}  1  +  i\mkleeneclose{}  0\mcdot{}  THENA  Auto))
  THEN  (InstLemma  `nth\_tl\_decomp\_eq`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RevHypSubst  (-1)  0  THENA  Auto)
  THEN  RWO  "append\_firstn\_lastn\_sq<"  0
  THEN  Auto)

---

Home Index