---

Step * 1 1 1 2 1 of Lemma list_split_iseg


1. [T] : Type
2. f : (T List) ⟶ 𝔹
3. ys : T List
4. y : T
5. v1 : T List List
6. v2 : T List
7. v3 : T List List
8. v4 : T List
9. v5 : T List List
10. v6 : T List
11. ((v1 = v5 ∈ (T List List)) ∧ v2 ≤ v6)
∨ (∃Z:T List. ∃ZZ:T List List. (((v1 @ [Z / ZZ]) = v5 ∈ (T List List)) ∧ v2 ≤ Z))
⊢ (if null(v6) then <v5, [y]>
if f v6 then <v5 @ [v6], [y]>
else <v5, v6 @ [y]>
fi 
= <v3, v4>
∈ (T List List × (T List)))
⇒ (((v1 = v3 ∈ (T List List)) ∧ v2 ≤ v4)
   ∨ (∃Z:T List. ∃ZZ:T List List. (((v1 @ [Z / ZZ]) = v3 ∈ (T List List)) ∧ v2 ≤ Z)))
BY
{ xxx(SplitOnConclITE THENA Auto)xxx }

1
.....truecase..... 
1. [T] : Type
2. f : (T List) ⟶ 𝔹
3. ys : T List
4. y : T
5. v1 : T List List
6. v2 : T List
7. v3 : T List List
8. v4 : T List
9. v5 : T List List
10. v6 : T List
11. ((v1 = v5 ∈ (T List List)) ∧ v2 ≤ v6)
∨ (∃Z:T List. ∃ZZ:T List List. (((v1 @ [Z / ZZ]) = v5 ∈ (T List List)) ∧ v2 ≤ Z))
12. v6 = [] ∈ (T List)
⊢ (<v5, [y]> = <v3, v4> ∈ (T List List × (T List)))
⇒ (((v1 = v3 ∈ (T List List)) ∧ v2 ≤ v4)
   ∨ (∃Z:T List. ∃ZZ:T List List. (((v1 @ [Z / ZZ]) = v3 ∈ (T List List)) ∧ v2 ≤ Z)))

2
.....falsecase..... 
1. [T] : Type
2. f : (T List) ⟶ 𝔹
3. ys : T List
4. y : T
5. v1 : T List List
6. v2 : T List
7. v3 : T List List
8. v4 : T List
9. v5 : T List List
10. v6 : T List
11. ((v1 = v5 ∈ (T List List)) ∧ v2 ≤ v6)
∨ (∃Z:T List. ∃ZZ:T List List. (((v1 @ [Z / ZZ]) = v5 ∈ (T List List)) ∧ v2 ≤ Z))
12. ¬(v6 = [] ∈ (T List))
⊢ (if f v6 then <v5 @ [v6], [y]> else <v5, v6 @ [y]> fi  = <v3, v4> ∈ (T List List × (T List)))
⇒ (((v1 = v3 ∈ (T List List)) ∧ v2 ≤ v4)
   ∨ (∃Z:T List. ∃ZZ:T List List. (((v1 @ [Z / ZZ]) = v3 ∈ (T List List)) ∧ v2 ≤ Z)))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  f  :  (T  List)  {}\mrightarrow{}  \mBbbB{}
3.  ys  :  T  List
4.  y  :  T
5.  v1  :  T  List  List
6.  v2  :  T  List
7.  v3  :  T  List  List
8.  v4  :  T  List
9.  v5  :  T  List  List
10.  v6  :  T  List
11.  ((v1  =  v5)  \mwedge{}  v2  \mleq{}  v6)  \mvee{}  (\mexists{}Z:T  List.  \mexists{}ZZ:T  List  List.  (((v1  @  [Z  /  ZZ])  =  v5)  \mwedge{}  v2  \mleq{}  Z))
\mvdash{}  (if  null(v6)  then  <v5,  [y]>  if  f  v6  then  <v5  @  [v6],  [y]>  else  <v5,  v6  @  [y]>  fi    =  <v3,  v4>)
{}\mRightarrow{}  (((v1  =  v3)  \mwedge{}  v2  \mleq{}  v4)  \mvee{}  (\mexists{}Z:T  List.  \mexists{}ZZ:T  List  List.  (((v1  @  [Z  /  ZZ])  =  v3)  \mwedge{}  v2  \mleq{}  Z)))


By

---

Latex:
xxx(SplitOnConclITE  THENA  Auto)xxx

---

Home Index