---

Step * 2 3 1 2 2 2 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 ∈ fpf-domain(if u ∈b v1 then 0 : v else ⊗ fi )))
∧ (∃v@0:V
    (may consider v@0 in inning 0 based on knowledge (mk_fpf(A;λb.<0, inr ⋅ >))
    ∧ (if (IdDeq u u) ∨bu ∈b v1 then 0 : v else ⊗ fi  = if u ∈b v1 then 0 : v else ⊗ fi  ⊕ 0 : v@0 ∈ i:ℤ fp-> V)))
BY
{ AutoBoolCase ⌜u ∈b v1⌝⋅ }

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)
⊢ (¬(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)))

---

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{}  (\mneg{}(0  \mmember{}  fpf-domain(if  u  \mmember{}\msubb{}  v1  then  0  :  v  else  \motimes{}  fi  )))
\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{}u  \mmember{}\msubb{}  v1  then  0  :  v  else  \motimes{}  fi 
            =  if  u  \mmember{}\msubb{}  v1  then  0  :  v  else  \motimes{}  fi    \moplus{}  0  :  v@0)))


By

---

Latex:
AutoBoolCase  \mkleeneopen{}u  \mmember{}\msubb{}  v1\mkleeneclose{}\mcdot{}

---

Home Index