---

Step * 1 1 1 of Lemma accum_split_iseg


1. [T] : Type
2. [A] : Type
3. g : (T List × A) ⟶ A
4. f : (T List × A) ⟶ 𝔹
5. v1 : (T List × A) List
6. v3 : T List
7. v4 : A
8. v5 : (T List × A) List
9. v7 : T List
10. v8 : A
11. <v1, v3, v4> = <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
{ (InstLemma `iseg_weakening` [] THEN OrLeft THEN Auto) }

---

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.  v1  :  (T  List  \mtimes{}  A)  List
6.  v3  :  T  List
7.  v4  :  A
8.  v5  :  (T  List  \mtimes{}  A)  List
9.  v7  :  T  List
10.  v8  :  A
11.  <v1,  v3,  v4>  =  <v5,  v7,  v8>
\mvdash{}  ((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:
(InstLemma  `iseg\_weakening`  []  THEN  OrLeft  THEN  Auto)

---

Home Index