--- presupposes finite_multiset.occ

( Marking : {V : Type}{C : V -> Type} Type )

---

( m_nil : {V | Type}{C | V -> Type}(Marking V C) )

( m_place : {V | Type}{C | V -> Type}{v : V}(fms (C v)) -> (Marking V C) )

( m_union : {V | Type}{C | V -> Type}(Marking V C) -> (Marking V C) -> (Marking V C) )

---

( m_union_is_comm : || {V : Type}{C : V -> Type}{m,m' : (Marking V C)}
  ((m_union m m') = (m_union m' m)) )

( m_union_is_assoc : || {V : Type}{C : V -> Type}{m,m',m'' : (Marking V C)}
  ((m_union m (m_union m' m'')) = (m_union (m_union m m') m'')) )

( m_union_id : !! {V : Type}{C : V -> Type}{m : (Marking V C)}
  ((m_union m (m_nil | V | C)) = m) )

---

( m_empty : {V | Type}{C | V -> Type}(Marking V C) -> Prop )

( m_empty_nil : ?? {V : Type}{C : V -> Type} (m_empty (m_nil | V | C)) )

( m_not_empty_single : ??  {V : Type}{C : V -> Type}{m : (Marking V C)}{v : V}{x : (fms (C v))}
  (Not (fms_empty x)) ->
  (Not (m_empty (m_union m (m_place v x)))) )

---

( m_le : {V | Type}{C | V -> Type}(Marking V C) -> (Marking V C) -> Prop)

---

( m_add : {V | Type}{C | V -> Type}
  (Marking V C) -> {v : V}(fms (C v)) -> (Marking V C) )

( m_add_ax : !! {V : Type}{C : V -> Type}{m : (Marking V C)}{v : V}{x : (fms (C v))}
  ((m_add m v x) = (m_union m (m_place v x))) )

---

( m_minus : {V | Type}{C | V -> Type}
  (Marking V C) -> (Marking V C) -> (Marking V C) )

( m_minus_nil : !! {V : Type}{C : V -> Type}{m : (Marking V C)}
  ((m_minus m (m_nil | V | C)) = m) ) 

*** ...

( m_minus_union : !! {V : Type}{C : V -> Type}{m,m' : (Marking V C)}
  (m_le m m') -> ((m_union (m_minus m' m) m) = m') )

( m_union_minus : !! {V : Type}{C : V -> Type}{m,m' : (Marking V C)}
  ((m_minus (m_union m' m) m) = m') )

---

( m_proj : {V | Type}{C | V -> Type}(Marking V C) -> {v : V}(fms (C v)) )

( m_proj_nil : !! {V : Type}{C : V -> Type}{v : V}
  ((m_proj (m_nil | V | C) v) = (fms_nil | (C v))) )

( m_proj_single_1 : !! {V : Type}{C : V -> Type}{v,v' : V}{b : (fms (C v'))}
  (!! (v = v')) -> ((m_proj (m_place v b) v') = b) )

( m_proj_single_2 : !! {V : Type}{C : V -> Type}{v,v' : V}{b : (fms (C v))}
  (Not (v = v')) -> ((m_proj (m_place v b) v') = (fms_nil | (C v'))) )

( m_proj_union : !! {V : Type}{C : V -> Type}{m,m' : (Marking V C)}{v : V}
  ((m_proj (m_union m m') v) =
      (fms_union (m_proj m v) (m_proj m' v))) )

( m_proj_minus : !! {V : Type}{C : V -> Type}{m,m' : (Marking V C)}{v : V}
  ((m_proj (m_minus m m') v) =
      (fms_minus (m_proj m v) (m_proj m' v))) )

---

( m_le_char : {V : Type}{C : V -> Type}{m,m' : (Marking V C)}
  (Iff (m_le m m') (All ? [v : V](fms_le (m_proj m v) (m_proj m' v)))) )

( m_union_resp_eq : {V : Type}{C : V -> Type}{m,n,m',n' : (Marking V C)}
  (m = m') -> (n = n') ->
  ((m_union m n) = (m_union m' n')) )

( m_le_union : {V : Type}{C : V -> Type}{m,m' : (Marking V C)}
  (m_le m' (m_union m m')) )

( m_le_imp_union : {V : Type}{C : V -> Type}{m,m' : (Marking V C)}
  (m_le m m') -> (Ex ? ([m'' : (Marking V C)] (m' = (m_union m m'')))) )

---

( m_single := [V | Type][C | V -> Type][v : V][x : (C v)] (m_place v (fms_single x)) ) 

--- place linearity equations

( m_place_linearity_0 : !! {V : Type}{C : V -> Type}{v : V} 
   ((m_place | V | C v (fms_nil | (C v))) = (m_nil | V | C)) )

( m_place_linearity_1 : !! {V : Type}{C : V -> Type}{v : V}{b,b' : (fms (C v))}
   (Not (fms_empty b)) -> (Not (fms_empty b')) ->
   ((m_place | V | C v (fms_union | (C v) b b')) = 
       (m_union | V | C (m_place | V | C v b) (m_place | V | C v b'))) )

( done )