---

Step * of Lemma iseg_filter2

∀[T:Type]
  ∀L_1,L_2:T List. ∀P:{x:T| (x ∈ L_1)}  ⟶ 𝔹.
    (L_2 ≤ filter(P;L_1) ⇒ (∃L_3:T List. (L_3 ≤ L_1 ∧ (L_2 = filter(P;L_3) ∈ (T List)))))
BY
{ (Intro
   THEN InstLemma `list_induction` [⌜T⌝;⌜λ2L_1.∀L_2:T List. ∀P:{x:T| (x ∈ L_1)}  ⟶ 𝔹.
                                                 (L_2 ≤ filter(P;L_1)
                                                 ⇒ (∃L_3:T List. (L_3 ≤ L_1 ∧ (L_2 = filter(P;L_3) ∈ (T List)))))⌝]⋅
   THEN Auto
   THEN Try ((SubsumeC  ⌜{x:T| (x ∈ L_3)}  List⌝⋅ THEN Auto))) }

1
1. [T] : Type
2. L_2 : T List
3. P : {x:T| (x ∈ [])}  ⟶ 𝔹
4. L_2 ≤ filter(P;[])
⊢ ∃L_3:T List. (L_3 ≤ [] ∧ (L_2 = filter(P;L_3) ∈ (T List)))

2
1. [T] : Type
2. aaaa : T
3. LLLL : T List
4. ∀L_2:T List. ∀P:{x:T| (x ∈ LLLL)}  ⟶ 𝔹.
     (L_2 ≤ filter(P;LLLL) ⇒ (∃L_3:T List. (L_3 ≤ LLLL ∧ (L_2 = filter(P;L_3) ∈ (T List)))))
5. L_2 : T List
6. P : {x:T| (x ∈ [aaaa / LLLL])}  ⟶ 𝔹
7. L_2 ≤ filter(P;[aaaa / LLLL])
⊢ ∃L_3:T List. (L_3 ≤ [aaaa / LLLL] ∧ (L_2 = filter(P;L_3) ∈ (T List)))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}L$_{1}$,L$_{2}$:T  List.  \mforall{}P:\{x:T|  (x  \mmember{}  L$_{1\mbackslash{}f\000Cf7d$)\}    {}\mrightarrow{}  \mBbbB{}.
        (L$_{2}$  \mleq{}  filter(P;L$_{1}$)  {}\mRightarrow{}  (\mexists{}L$_{3}\000C$:T  List.  (L$_{3}$  \mleq{}  L$_{1}$  \mwedge{}  (L$_{2}\mbackslash{}f\000Cf24  =  filter(P;L$_{3}$)))))


By

---

Latex:
(Intro
  THEN  InstLemma  `list\_induction`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}L$_{1}$.\mforall{}L$_{2}$:T  \000CList.  \mforall{}P:\{x:T|  (x  \mmember{}  L$_{1}$)\}    {}\mrightarrow{}  \mBbbB{}.
                                                                                            (L$_{2}$  \mleq{}  filter(P;L$_\mbackslash{}ff\000C7b1}$)
                                                                                            {}\mRightarrow{}  (\mexists{}L$_{3}$:T  List.  (L$_\mbackslash{}\000Cff7b3}$  \mleq{}  L$_{1}$  \mwedge{}  (L$_{2}$  =  filter(P;L$_\mbackslash{}\000Cff7b3}$)))))\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  ((SubsumeC    \mkleeneopen{}\{x:T|  (x  \mmember{}  L$_{3}$)\}    List\mkleeneclose{}\mcdot{}  THEN  Auto)))

---

Home Index