---

Step * 1 1 2 1 of Lemma accum_split_iseg


1. [T] : Type
2. [A] : Type
3. g : (T List × A) ⟶ A
4. f : (T List × A) ⟶ 𝔹
5. ys : T List
6. y : T
7. v1 : (T List × A) List
8. v3 : T List
9. v4 : A
10. v5 : (T List × A) List
11. v7 : T List
12. v8 : A
13. v9 : (T List × A) List
14. v11 : T List
15. v12 : A
16. ((v1 = v9 ∈ ((T List × A) List)) ∧ v3 ≤ v11 ∧ (v4 = v12 ∈ A))
∨ (∃Z:T List. ∃ZZ:(T List × A) List. (((v1 @ [<Z, v4> / ZZ]) = v9 ∈ ((T List × A) List)) ∧ v3 ≤ Z))
⊢ (if null(v11) then <v9, [y], v12>
if f <v11, v12> then <v9 @ [<v11, v12>], [y], g <v11, v12>>
else <v9, v11 @ [y], v12>
fi 
= <v5, v7, v8>
∈ ((T List × A) List × T List × A))
⇒ (((v1 = v5 ∈ ((T List × A) List)) ∧ v3 ≤ v7 ∧ (v4 = v8 ∈ A))
   ∨ (∃Z:T List. ∃ZZ:(T List × A) List. (((v1 @ [<Z, v4> / ZZ]) = v5 ∈ ((T List × A) List)) ∧ v3 ≤ Z)))
BY
{ (SplitOnConclITE THENA Auto) }

1
.....truecase..... 
1. [T] : Type
2. [A] : Type
3. g : (T List × A) ⟶ A
4. f : (T List × A) ⟶ 𝔹
5. ys : T List
6. y : T
7. v1 : (T List × A) List
8. v3 : T List
9. v4 : A
10. v5 : (T List × A) List
11. v7 : T List
12. v8 : A
13. v9 : (T List × A) List
14. v11 : T List
15. v12 : A
16. ((v1 = v9 ∈ ((T List × A) List)) ∧ v3 ≤ v11 ∧ (v4 = v12 ∈ A))
∨ (∃Z:T List. ∃ZZ:(T List × A) List. (((v1 @ [<Z, v4> / ZZ]) = v9 ∈ ((T List × A) List)) ∧ v3 ≤ Z))
17. v11 = [] ∈ (T List)
⊢ (<v9, [y], v12> = <v5, v7, v8> ∈ ((T List × A) List × T List × A))
⇒ (((v1 = v5 ∈ ((T List × A) List)) ∧ v3 ≤ v7 ∧ (v4 = v8 ∈ A))
   ∨ (∃Z:T List. ∃ZZ:(T List × A) List. (((v1 @ [<Z, v4> / ZZ]) = v5 ∈ ((T List × A) List)) ∧ v3 ≤ Z)))

2
.....falsecase..... 
1. [T] : Type
2. [A] : Type
3. g : (T List × A) ⟶ A
4. f : (T List × A) ⟶ 𝔹
5. ys : T List
6. y : T
7. v1 : (T List × A) List
8. v3 : T List
9. v4 : A
10. v5 : (T List × A) List
11. v7 : T List
12. v8 : A
13. v9 : (T List × A) List
14. v11 : T List
15. v12 : A
16. ((v1 = v9 ∈ ((T List × A) List)) ∧ v3 ≤ v11 ∧ (v4 = v12 ∈ A))
∨ (∃Z:T List. ∃ZZ:(T List × A) List. (((v1 @ [<Z, v4> / ZZ]) = v9 ∈ ((T List × A) List)) ∧ v3 ≤ Z))
17. ¬(v11 = [] ∈ (T List))
⊢ (if f <v11, v12> then <v9 @ [<v11, v12>], [y], g <v11, v12>> else <v9, v11 @ [y], v12> fi 
= <v5, v7, v8>
∈ ((T List × A) List × T List × A))
⇒ (((v1 = v5 ∈ ((T List × A) List)) ∧ v3 ≤ v7 ∧ (v4 = v8 ∈ A))
   ∨ (∃Z:T List. ∃ZZ:(T List × A) List. (((v1 @ [<Z, v4> / ZZ]) = v5 ∈ ((T List × A) List)) ∧ v3 ≤ Z)))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [A]  :  Type
3.  g  :  (T  List  \mtimes{}  A)  {}\mrightarrow{}  A
4.  f  :  (T  List  \mtimes{}  A)  {}\mrightarrow{}  \mBbbB{}
5.  ys  :  T  List
6.  y  :  T
7.  v1  :  (T  List  \mtimes{}  A)  List
8.  v3  :  T  List
9.  v4  :  A
10.  v5  :  (T  List  \mtimes{}  A)  List
11.  v7  :  T  List
12.  v8  :  A
13.  v9  :  (T  List  \mtimes{}  A)  List
14.  v11  :  T  List
15.  v12  :  A
16.  ((v1  =  v9)  \mwedge{}  v3  \mleq{}  v11  \mwedge{}  (v4  =  v12))
\mvee{}  (\mexists{}Z:T  List.  \mexists{}ZZ:(T  List  \mtimes{}  A)  List.  (((v1  @  [<Z,  v4>  /  ZZ])  =  v9)  \mwedge{}  v3  \mleq{}  Z))
\mvdash{}  (if  null(v11)  then  <v9,  [y],  v12>
if  f  <v11,  v12>  then  <v9  @  [<v11,  v12>],  [y],  g  <v11,  v12>>
else  <v9,  v11  @  [y],  v12>
fi 
=  <v5,  v7,  v8>)
{}\mRightarrow{}  (((v1  =  v5)  \mwedge{}  v3  \mleq{}  v7  \mwedge{}  (v4  =  v8))
      \mvee{}  (\mexists{}Z:T  List.  \mexists{}ZZ:(T  List  \mtimes{}  A)  List.  (((v1  @  [<Z,  v4>  /  ZZ])  =  v5)  \mwedge{}  v3  \mleq{}  Z)))


By

---

Latex:
(SplitOnConclITE  THENA  Auto)

---

Home Index