---

Step * 2 3 1 2 2 2 1 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)
11. ¬(u ∈ v1)
12. u = u ∈ Id
13. ¬(0 ∈ [])
⊢ ∃v@0:V
   (may consider v@0 in inning 0 based on knowledge (mk_fpf(A;λb.<0, inr ⋅ >)) ∧ (0 : v = ⊗ ⊕ 0 : v@0 ∈ i:ℤ fp-> V))
BY
{ (InstConcl [⌜v⌝]⋅ THEN Auto) }

1
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)
11. ¬(u ∈ v1)
12. u = u ∈ Id
13. ¬(0 ∈ [])
⊢ may consider v in inning 0 based on knowledge (mk_fpf(A;λb.<0, inr ⋅ >))

---

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)
11.  \mneg{}(u  \mmember{}  v1)
12.  u  =  u
13.  \mneg{}(0  \mmember{}  [])
\mvdash{}  \mexists{}v@0:V
      (may  consider  v@0  in  inning  0  based  on  knowledge  (mk\_fpf(A;\mlambda{}b.ɘ,  inr  \mcdot{}  >))
      \mwedge{}  (0  :  v  =  \motimes{}  \moplus{}  0  :  v@0))


By

---

Latex:
(InstConcl  [\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index