---

Step * 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]))
⊢ ∃K,J:T List. ((L = (K @ [x / J]) ∈ (T List)) ∧ (↑(P x)) ∧ (∀y∈K.¬↑(P y)))
BY
{ TACTIC:TACTIC:(InstConcl [⌜firstn(i;L)⌝;⌜nth_tl(i + 1;L)⌝]⋅ THEN Auto) }

1
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)

2
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]))
9. L = (firstn(i;L) @ [x / nth_tl(i + 1;L)]) ∈ (T List)
10. ↑(P x)
⊢ (∀y∈firstn(i;L).¬↑(P y))

---

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{}  \mexists{}K,J:T  List.  ((L  =  (K  @  [x  /  J]))  \mwedge{}  (\muparrow{}(P  x))  \mwedge{}  (\mforall{}y\mmember{}K.\mneg{}\muparrow{}(P  y)))


By

---

Latex:
TACTIC:TACTIC:(InstConcl  [\mkleeneopen{}firstn(i;L)\mkleeneclose{};\mkleeneopen{}nth\_tl(i  +  1;L)\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index