---

Step * 1 2 of Lemma first-member-cons


1. [T] : Type
2. P : T ⟶ 𝔹
3. x : T
4. u : T
5. L : T List
6. i : ℕ||[u / L]||
7. (x = [u / L][i] ∈ T) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P [u / L][j])))
8. ¬(i = 0 ∈ ℤ)
⊢ if P u then x = u ∈ T else first-member(T;x;L;P) fi 
BY
{ xxx(Auto
      THEN RWO "select-cons-tl" (-4)
      THEN Auto
      THEN (InstHyp [⌜0⌝] (-2)⋅ THENA Auto)
      THEN Reduce (-1)
      THEN AutoSplit
      THEN With ⌜i - 1⌝ (D 0)⋅
      THEN Auto
      THEN Auto')xxx }

1
1. T : Type
2. P : T ⟶ 𝔹
3. x : T
4. u : T
5. ¬↑(P u)
6. L : T List
7. i : ℕ||[u / L]||
8. x = L[i - 1] ∈ T
9. ↑(P x)
10. ∀j:ℕi. (¬↑(P [u / L][j]))
11. ¬(i = 0 ∈ ℤ)
12. ¬False
13. x = L[i - 1] ∈ T
14. ↑(P x)
15. j : ℕi - 1
⊢ ¬↑(P L[j])

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  x  :  T
4.  u  :  T
5.  L  :  T  List
6.  i  :  \mBbbN{}||[u  /  L]||
7.  (x  =  [u  /  L][i])  \mwedge{}  (\muparrow{}(P  x))  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}(P  [u  /  L][j])))
8.  \mneg{}(i  =  0)
\mvdash{}  if  P  u  then  x  =  u  else  first-member(T;x;L;P)  fi 


By

---

Latex:
xxx(Auto
        THEN  RWO  "select-cons-tl"  (-4)
        THEN  Auto
        THEN  (InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
        THEN  Reduce  (-1)
        THEN  AutoSplit
        THEN  With  \mkleeneopen{}i  -  1\mkleeneclose{}  (D  0)\mcdot{}
        THEN  Auto
        THEN  Auto')xxx

---

Home Index