---

Step * 2 3 1 2 2 1 of Lemma cs-possible-state-reachable


1. V : Type
2. A : Id List
3. W : {a:Id| (a ∈ A)}  List List
4. v : V
5. 1 < ||W||
6. two-intersection(A;W)
7. u : Id@i
8. [%6] : (u ∈ A)@i
9. v1 : {a:Id| (a ∈ A)}  List@i
10. ¬(u ∈ v1)
⊢ (0 = 0 ∈ ℤ) ∧ (mk_fpf(A;λb.<0, inr ⋅ >) = mk_fpf(A;λb.<0, inr ⋅ >) ∈ b:Id fp-> ℤ × (ℤ × V + Top))
BY
{ Auto }

---

Latex:

---

Latex:

1.  V  :  Type
2.  A  :  Id  List
3.  W  :  \{a:Id|  (a  \mmember{}  A)\}    List  List
4.  v  :  V
5.  1  <  ||W||
6.  two-intersection(A;W)
7.  u  :  Id@i
8.  [\%6]  :  (u  \mmember{}  A)@i
9.  v1  :  \{a:Id|  (a  \mmember{}  A)\}    List@i
10.  \mneg{}(u  \mmember{}  v1)
\mvdash{}  (0  =  0)  \mwedge{}  (mk\_fpf(A;\mlambda{}b.ɘ,  inr  \mcdot{}  >)  =  mk\_fpf(A;\mlambda{}b.ɘ,  inr  \mcdot{}  >))


By

---

Latex:
Auto

---

Home Index