---

Step * 1 of Lemma general-append-cancellation


1. T : Type
2. bs : T List
3. cs : T List
4. ds : T List
5. cs = (bs @ ds) ∈ (T List)
6. (0 = ||bs|| ∈ ℤ) ∨ (||cs|| = ||ds|| ∈ ℤ)
⊢ {([] = bs ∈ (T List)) ∧ (cs = ds ∈ (T List))}
BY
{ (DVar `bs'
   THEN All Reduce
   THEN Unfold `guard` 0
   THEN Try (Complete (Auto))
   THEN Assert ⌜False⌝⋅
   THEN Auto
   THEN (D (-1))
   THEN Auto) }

1
1. T : Type
2. u : T
3. v : T List
4. cs : T List
5. ds : T List
6. cs = [u / (v @ ds)] ∈ (T List)
7. 0 = (||v|| + 1) ∈ ℤ
⊢ False

2
1. T : Type
2. u : T
3. v : T List
4. cs : T List
5. ds : T List
6. cs = [u / (v @ ds)] ∈ (T List)
7. ||cs|| = ||ds|| ∈ ℤ
⊢ False

---

Latex:

---

Latex:

1.  T  :  Type
2.  bs  :  T  List
3.  cs  :  T  List
4.  ds  :  T  List
5.  cs  =  (bs  @  ds)
6.  (0  =  ||bs||)  \mvee{}  (||cs||  =  ||ds||)
\mvdash{}  \{([]  =  bs)  \mwedge{}  (cs  =  ds)\}


By

---

Latex:
(DVar  `bs'
  THEN  All  Reduce
  THEN  Unfold  `guard`  0
  THEN  Try  (Complete  (Auto))
  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  (D  (-1))
  THEN  Auto)

---

Home Index