---

Step * 1 1 2 1 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. 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)
17. v3 ≤ v11
18. v4 = v12 ∈ A
19. v11 = [] ∈ (T List)
20. v9 = v5 ∈ ((T List × A) List)
21. [y] = v7 ∈ (T List)
22. v12 = v8 ∈ A
23. v1 = v5 ∈ ((T List × A) List)
⊢ v3 ≤ v7
BY
{ ((Assert v3 ≤ [] BY
          Auto)
   THEN FLemma `iseg_nil` [-1]
   THEN Auto
   THEN RW assert_pushdownC (-1)
   THEN Auto
   THEN HypSubst (-1) 0
   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.  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
17.  v3  \mleq{}  v11
18.  v4  =  v12
19.  v11  =  []
20.  v9  =  v5
21.  [y]  =  v7
22.  v12  =  v8
23.  v1  =  v5
\mvdash{}  v3  \mleq{}  v7


By

---

Latex:
((Assert  v3  \mleq{}  []  BY
                Auto)
  THEN  FLemma  `iseg\_nil`  [-1]
  THEN  Auto
  THEN  RW  assert\_pushdownC  (-1)
  THEN  Auto
  THEN  HypSubst  (-1)  0
  THEN  Auto)

---

Home Index