---

Step * 2 3 1 2 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)
11. ¬(u ∈ v1)
⊢ (¬(0 ∈ []))
∧ (∃v@0:V
    (may consider v@0 in inning 0 based on knowledge (mk_fpf(A;λb.<0, inr ⋅ >))
    ∧ (if (IdDeq u u) ∨bff then 0 : v else ⊗ fi  = ⊗ ⊕ 0 : v@0 ∈ i:ℤ fp-> V)))
BY
{ (Try (Unfold `eqof` 0) THEN (Fold `eq_id` 0 THEN AutoBoolCase ⌜u = u⌝⋅) 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 ∈ [])
⊢ ∃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))

---

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)
\mvdash{}  (\mneg{}(0  \mmember{}  []))
\mwedge{}  (\mexists{}v@0:V
        (may  consider  v@0  in  inning  0  based  on  knowledge  (mk\_fpf(A;\mlambda{}b.ɘ,  inr  \mcdot{}  >))
        \mwedge{}  (if  (IdDeq  u  u)  \mvee{}\msubb{}ff  then  0  :  v  else  \motimes{}  fi    =  \motimes{}  \moplus{}  0  :  v@0)))


By

---

Latex:
(Try  (Unfold  `eqof`  0)  THEN  (Fold  `eq\_id`  0  THEN  AutoBoolCase  \mkleeneopen{}u  =  u\mkleeneclose{}\mcdot{})  THEN  Auto)

---

Home Index