---

Step * 2 1 of Lemma filter_iseg


1. [T] : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ∀L1:T List. (L1 ≤ v ⇒ filter(P;L1) ≤ filter(P;v))
6. u1 : T
7. v1 : T List
8. v1 ≤ [u / v] ⇒ filter(P;v1) ≤ if P u then [u / filter(P;v)] else filter(P;v) fi 
9. [u1 / v1] ≤ [u / v]
⊢ if P u1 then [u1 / filter(P;v1)] else filter(P;v1) fi  ≤ if P u then [u / filter(P;v)] else filter(P;v) fi 
BY
{ ((((((RWO "cons_iseg" (-1) THENA Auto) THEN D (-1)) THEN HypSubst (-2) 0) THENA Auto) THEN SplitOnConclITE)
   THENA Auto
   ) }

1
.....truecase..... 
1. [T] : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ∀L1:T List. (L1 ≤ v ⇒ filter(P;L1) ≤ filter(P;v))
6. u1 : T
7. v1 : T List
8. v1 ≤ [u / v] ⇒ filter(P;v1) ≤ if P u then [u / filter(P;v)] else filter(P;v) fi 
9. u1 = u ∈ T
10. v1 ≤ v
11. ↑(P u)
⊢ [u / filter(P;v1)] ≤ [u / filter(P;v)]

2
.....falsecase..... 
1. [T] : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ∀L1:T List. (L1 ≤ v ⇒ filter(P;L1) ≤ filter(P;v))
6. u1 : T
7. v1 : T List
8. v1 ≤ [u / v] ⇒ filter(P;v1) ≤ if P u then [u / filter(P;v)] else filter(P;v) fi 
9. u1 = u ∈ T
10. v1 ≤ v
11. ¬↑(P u)
⊢ filter(P;v1) ≤ filter(P;v)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}L1:T  List.  (L1  \mleq{}  v  {}\mRightarrow{}  filter(P;L1)  \mleq{}  filter(P;v))
6.  u1  :  T
7.  v1  :  T  List
8.  v1  \mleq{}  [u  /  v]  {}\mRightarrow{}  filter(P;v1)  \mleq{}  if  P  u  then  [u  /  filter(P;v)]  else  filter(P;v)  fi 
9.  [u1  /  v1]  \mleq{}  [u  /  v]
\mvdash{}  if  P  u1  then  [u1  /  filter(P;v1)]  else  filter(P;v1)  fi    \mleq{}  if  P  u
    then  [u  /  filter(P;v)]
    else  filter(P;v)
    fi 


By

---

Latex:
((((((RWO  "cons\_iseg"  (-1)  THENA  Auto)  THEN  D  (-1))  THEN  HypSubst  (-2)  0)  THENA  Auto)
    THEN  SplitOnConclITE
    )
  THENA  Auto
  )

---

Home Index