---

Step * 3 of Lemma iseg_filter_last


1. [T] : Type
2. P : T ⟶ 𝔹
3. u : T
4. ¬↑(P u)
5. v : T List
6. ∀L_2:T List
     (0 < ||L_2||
     ⇒ L_2 ≤ filter(P;v)
     ⇒ (∃L_3:T List. (L_3 ≤ v ∧ (L_2 = filter(P;L_3) ∈ (T List)) ∧ 0 < ||L_3|| ∧ (last(L_2) = last(L_3) ∈ T))))
7. L_2 : T List
8. 0 < ||L_2||
9. L_2 ≤ filter(P;v)
⊢ ∃L_3:T List. (L_3 ≤ [u / v] ∧ (L_2 = filter(P;L_3) ∈ (T List)) ∧ 0 < ||L_3|| ∧ (last(L_2) = last(L_3) ∈ T))
BY
{ TACTIC:((InstHyp [⌜L_2⌝] (-4)⋅ THENA Auto) THEN ExRepD THEN InstConcl [[u / L_3]] THEN Auto) }

1
1. [T] : Type
2. P : T ⟶ 𝔹
3. u : T
4. ¬↑(P u)
5. v : T List
6. ∀L_2:T List
     (0 < ||L_2||
     ⇒ L_2 ≤ filter(P;v)
     ⇒ (∃L_3:T List. (L_3 ≤ v ∧ (L_2 = filter(P;L_3) ∈ (T List)) ∧ 0 < ||L_3|| ∧ (last(L_2) = last(L_3) ∈ T))))
7. L_2 : T List
8. 0 < ||L_2||
9. L_2 ≤ filter(P;v)
10. L_3 : T List
11. L_3 ≤ v
12. L_2 = filter(P;L_3) ∈ (T List)
13. 0 < ||L_3||
14. last(L_2) = last(L_3) ∈ T
⊢ [u / L_3] ≤ [u / v]

2
1. T : Type
2. P : T ⟶ 𝔹
3. u : T
4. ¬↑(P u)
5. v : T List
6. ∀L_2:T List
     (0 < ||L_2||
     ⇒ L_2 ≤ filter(P;v)
     ⇒ (∃L_3:T List. (L_3 ≤ v ∧ (L_2 = filter(P;L_3) ∈ (T List)) ∧ 0 < ||L_3|| ∧ (last(L_2) = last(L_3) ∈ T))))
7. L_2 : T List
8. 0 < ||L_2||
9. L_2 ≤ filter(P;v)
10. L_3 : T List
11. L_3 ≤ v
12. L_2 = filter(P;L_3) ∈ (T List)
13. 0 < ||L_3||
14. last(L_2) = last(L_3) ∈ T
15. [u / L_3] ≤ [u / v]
⊢ L_2 = filter(P;[u / L_3]) ∈ (T List)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  u  :  T
4.  \mneg{}\muparrow{}(P  u)
5.  v  :  T  List
6.  \mforall{}L$_{2}$:T  List
          (0  <  ||L$_{2}$||
          {}\mRightarrow{}  L$_{2}$  \mleq{}  filter(P;v)
          {}\mRightarrow{}  (\mexists{}L$_{3}$:T  List.  (L$_{3}$  \mleq{}  v  \mwedge{}  (L$_{2\mbackslash{}\000Cff7d$  =  filter(P;L$_{3}$))  \mwedge{}  0  <  ||L$_{3}$||  \mwedge{}  (last(L\mbackslash{}f\000Cf24_{2}$)  =  last(L$_{3}$)))))
7.  L$_{2}$  :  T  List
8.  0  <  ||L$_{2}$||
9.  L$_{2}$  \mleq{}  filter(P;v)
\mvdash{}  \mexists{}L$_{3}$:T  List.  (L$_{3}$  \mleq{}  [u  /  v]  \mwedge{}  (L$_{2\mbackslash{}f\000Cf7d$  =  filter(P;L$_{3}$))  \mwedge{}  0  <  ||L$_{3}$||  \mwedge{}  (last(L\mbackslash{}ff\000C24_{2}$)  =  last(L$_{3}$)))


By

---

Latex:
TACTIC:((InstHyp  [\mkleeneopen{}L$_{2}$\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)  THEN  ExRepD  THEN  InstConcl  [[u  /  \000CL$_{3}$]]  THEN  Auto)

---

Home Index