---

Step * 1 of Lemma sv-class-iff


1. Info : Type
2. A : es:EO+(Info) ─→ E ─→ Type
3. X : EClass(A[es;e])
4. Singlevalued(X)@i'
5. es : EO+(Info)@i'
6. e : E@i
⊢ (X es e) = if (#(X es e) =z 1) then X es e else {} fi  ∈ bag(A[es;e])
BY
{ ((Assert #(X es e) ≤ 1 BY Auto) THEN AutoSplit) }

1
1. Info : Type
2. A : es:EO+(Info) ─→ E ─→ Type
3. X : EClass(A[es;e])
4. Singlevalued(X)@i'
5. es : EO+(Info)@i'
6. e : E@i
7. (#(X es e) + 1) ≤ 1
⊢ (X es e) = {} ∈ bag(A[es;e])

---

Latex:



1.  Info  :  Type
2.  A  :  es:EO+(Info)  {}\mrightarrow{}  E  {}\mrightarrow{}  Type
3.  X  :  EClass(A[es;e])
4.  Singlevalued(X)@i'
5.  es  :  EO+(Info)@i'
6.  e  :  E@i
\mvdash{}  (X  es  e)  =  if  (\#(X  es  e)  =\msubz{}  1)  then  X  es  e  else  \{\}  fi 


By

((Assert  \#(X  es  e)  \mleq{}  1  BY  Auto)  THEN  AutoSplit)

---

Home Index