--- presupposes equality.occ
--- presupposes nat.occ

( fs : Type -> Type )

---

( fs_nil : {T | Type} (fs T) )

( fs_single : {T | Type} T -> (fs T) )

( fs_union : {T | Type} (fs T) -> (fs T) -> (fs T) )

---

( fs_union_comm : || {T : Type}{m1,m2 : (fs T)}
  ((fs_union m1 m2) = (fs_union m2 m1)) )

( fs_union_assoc : || {T : Type}{m1,m2,m3 : (fs T)}
  ((fs_union m1 (fs_union m2 m3)) = (fs_union (fs_union m1 m2) m3)) )

( fs_union_right_id : || {T : Type}{m : (fs T)} 
  ((fs_union m (fs_nil | T)) = m) )

( fs_union_left_id : || {T : Type}{m : (fs T)} 
  ((fs_union (fs_nil | T) m) = m) )

---

( fs_inj_single : ?? {T : Type}{x,y : T}
  (Not (x = y)) -> (Not ((fs_single x) = (fs_single y))) )

( fs_inj_union : ?? {T : Type}{x : T}{m,m' : (fs T)}
  (Not (m = m')) -> (Not ((fs_union (fs_single x) m) = (fs_union (fs_single x) m'))) )

---

( fs_empty : {U | Type} (fs U) -> Prop )

( fs_empty_nil : ?? {U : Type} (fs_empty | U (fs_nil | U)) )

( fs_not_empty_single : ?? {U : Type}{m : (fs U)}{u : U} 
  (Not (fs_empty | U (fs_union m (fs_single u)))) )

---

( fs_union_idemp : !! {T : Type}{x : T}
   ((fs_union (fs_single x) (fs_single x)) = (fs_single x)) )

---

( fs_in : {T | Type} (fs T) -> T -> Prop )

( fs_in_single : ?? {T : Type}{m : (fs T)}{x : T} 
  (fs_in (fs_union m (fs_single x)) x) )

( fs_in_union : ?? {T : Type}{m,m' : (fs T)}{x : T} 
  (Not (fs_empty m)) -> (Not (fs_empty m')) -> (Not (fs_in m x)) -> (fs_in m' x) -> 
  (fs_in (fs_union m m') x) )

( fs_not_in_nil : ?? {T : Type}{x : T} 
  (Not (fs_in (fs_nil | T) x)) )

( fs_not_in_single : ?? {T : Type}{x,y : T} 
  (Not (x = y)) -> (Not (fs_in (fs_single y) x)) )

( fs_not_in_union : ?? {T : Type}{m,m' : (fs T)}{x : T} 
  (Not (fs_empty m)) -> (Not (fs_empty m')) -> (Not (fs_in m x)) -> (Not (fs_in m' x)) -> 
  (Not (fs_in (fs_union m m') x)) )

---

( fs_le : {T | Type} (fs T) -> (fs T) -> Prop )

( fs_le_nil : ?? {T : Type}{m : (fs T)} 
  (fs_le (fs_nil | T) m) )

( fs_le_union_0 : ?? {T : Type}{m,m' : (fs T)}{x : T} 
  (fs_le m m') -> (fs_le (fs_union (fs_single x) m) (fs_union (fs_single x) m')) )

( fs_le_union_1 : ?? {T : Type}{m : (fs T)}{x : T} 
  (Not (fs_in m x)) -> (fs_le m (fs_union (fs_single x) m)) )

( fs_le_refl : ?? {T : Type}{m : (fs T)} 
  (fs_le m m) )

( fs_le_trans : {T : Type}{m,m',m'' : (fs T)} 
  (fs_le m m') -> (fs_le m' m'') -> (fs_le m m'') )

---

( fs_eq : {T | Type} (fs T) -> (fs T) -> Prop )

( fs_eq_0 : ?? {T : Type}{m,m' : (fs T)}
  (fs_le m m') -> (fs_le m' m) -> (fs_eq m m') )

( fs_not_eq_1 : ?? {U : Type}{u : U}{m : (fs U)} 
  (Not (fs_eq (fs_union m (fs_single u)) (fs_nil | U))) )

( fs_not_eq_2 : ?? {U : Type}{u : U}{m : (fs U)} 
  (Not (fs_eq (fs_nil | U) (fs_union m (fs_single u)))) )

( fs_not_eq_3 : ?? {U : Type}{u,v : U}{m1,m2 : (fs U)} (Not (u = v)) -> 
  (Not (fs_eq (fs_union (fs_single u) m1) (fs_union (fs_single v) m2))) )

( fs_not_eq_4 : ?? {U : Type}{u : U}{m1,m2 : (fs U)} (Not (fs_eq m1 m2)) -> 
  (Not (fs_eq (fs_union (fs_single u) m1) (fs_union (fs_single u) m2))) )

---

( fs_eq_implies_EQ : ?? {T : Type}{m,m' : (fs T)}
  (fs_eq m m') -> (m = m') )

( fs_not_eq_implies_not_EQ : ?? {T : Type}{m,m' : (fs T)}
  (Not (fs_eq m m')) -> (Not (m = m')) )

---

( fs_lt : {T | Type} (fs T) -> (fs T) -> Prop )

( fs_lt_ax : ?? {T : Type}{m,m' : (fs T)}
  (Not (fs_eq m m')) -> (fs_le m m') -> (fs_lt m m') )

( fs_lt_trans : {T : Type}{m,m',m'' : (fs T)} 
  (fs_lt m m') -> (fs_lt m' m'') -> (fs_lt m m'') )

---

( fs_card : {T | Type} (fs T) -> nat )

( fs_card_nil : !! {T : Type}{x : T} 
  ((fs_card (fs_nil | T)) = 0) )

( fs_card_single : !! {T : Type}{x : T} 
  ((fs_card (fs_single x)) = 1) )

( fs_card_union : !! {T : Type}{x : T}{m : (fs T)}
  (Not (fs_in m x)) -> ((fs_card (fs_union (fs_single x) m)) = (suc (fs_card m))) )

---

( fs_occ : {T | Type} (fs T) -> T -> nat )

( fs_occ_nil : !! {T : Type}{x : T} 
  ((fs_occ (fs_nil | T) x) = 0) ) 

( fs_occ_single_0 : !! {T : Type}{x,y : T} 
  (x = y) -> ((fs_occ (fs_single y) x) = 1) ) 

( fs_occ_single_1 : !! {T : Type}{x,y : T} 
  (Not (x = y)) -> ((fs_occ (fs_single y) x) = 0) ) 

( fs_occ_union : !! {T : Type}{m,m' : (fs T)}{x : T} 
  (Not (fs_empty m)) -> (Not (fs_empty m')) ->
  ((fs_occ (fs_union m m') x) = (nat_plus (fs_occ m x) (fs_occ m' x))) )

( fs_le_occ : {T : Type}{m,m' : (fs T)} 
  (fs_le m m') -> {x : T}(nat_le (fs_occ m x) (fs_occ m' x)) )

( fs_occ_le : {T : Type}{m,m' : (fs T)} 
  {x : T}(nat_le (fs_occ m x) (fs_occ m' x)) -> (fs_le m m'))

---

( fs_add : {T | Type} (fs T) -> T -> (fs T) )

( fs_add_single : !! {T : Type}{m : (fs T)}{x : T}
  ((fs_add m x) = (fs_union m (fs_single x))) )

( fs_in_add_eq : {T : Type}{m : (fs T)}{x : T} 
  (fs_in (fs_add m x) x) )

( fs_in_add_neq : {T : Type}{m : (fs T)}{x,y : T} (Not (x = y)) ->
  (fs_in (fs_add m x) y) -> (fs_in m y) )

---

( fs_single_inj : {T : Type}{x,y : T} 
  ((fs_single x) = (fs_single y)) -> (x = y) )

---

( fs_eq_occ := [T | Type][m,m' : (fs T)] {x : T}
  ((fs_occ m x) = (fs_occ m' x)) )

( fs_extensionality : {T : Type}{m,m' : (fs T)} 
  (fs_eq_occ m m') -> (m = m') )

---

( fs_in_union_l : {T : Type}{m,m' : (fs T)}{x : T} (fs_in m x) -> 
  (fs_in (fs_union m m') x) )

( fs_in_union_r : {T : Type}{m,m' : (fs T)}{x : T} (fs_in m' x) -> 
  (fs_in (fs_union m m') x) )

( fs_in_union : {T : Type}{m,m' : (fs T)}{x : T}
  (fs_in (fs_union m m') x) -> (Or (fs_in m x) (fs_in m' x)) )

( fs_le_single : {T : Type}{m : (fs T)}{x : T} 
  (fs_in m x) -> (fs_le (fs_single x) m) )

( fs_in_single_implies_eq : {T : Type}{x,y : T} 
  (fs_in (fs_single x) y) -> (x = y) )

---

( fs_minus : {T | Type} (fs T) -> (fs T) -> (fs T) )

( fs_minus_0 : !! {T : Type}{m : (fs T)} 
  ((fs_minus m (fs_nil | T)) = m) )

( fs_minus_1 : !! {T : Type}{m : (fs T)} 
  ((fs_minus (fs_nil | T) m) = (fs_nil | T)) )

( fs_minus_2 : !! {T : Type}{x : T}{m,m' : (fs T)} 
  ((fs_minus (fs_union (fs_single x) m) (fs_union (fs_single x) m') ) = (fs_minus m m') ) )

( fs_minus_3 : !! {T : Type}{x : T}{m,m' : (fs T)} 
  (Not (fs_in m x)) -> ((fs_minus m (fs_union (fs_single x) m') ) = (fs_minus m m')) )

( fs_union_minus : !! {T : Type}{m,m' : (fs T)} 
  ((fs_minus (fs_union m' m) m) = m') )

( fs_minus_union : {T : Type}{m,m' : (fs T)} (fs_le m m') -> 
  ((fs_union (fs_minus m' m) m) = m') )

( fs_occ_minus : {T : Type}{m,m' : (fs T)}{x : T}
  ((fs_occ (fs_minus m m') x) = (nat_minus (fs_occ m x) (fs_occ m' x))) )

---

( fs_mult : {T | Type}{n : nat} (fs T) -> (fs T) )

( fs_mult_0 : !! {T : Type}{m : (fs T)}
  ((fs_mult 0 m) = (fs_nil | T)) )

( fs_mult_1 : !! {T : Type}{n : nat}{m : (fs T)}
  ((fs_mult (suc n) m) = (fs_union (fs_mult n m) m)) )

( fs_occ_mult : {T : Type}{n : nat}{m : (fs T)}{x : T}
  ((fs_occ (fs_mult n m) x) = (nat_mult n (fs_occ m x))) )

--- 

( fs_map : {U,V | Type} (U -> V) -> (fs U) ->(fs V) )

( fs_map_nil : !! {U,V : Type}{f : (U -> V)}
  ((fs_map f (fs_nil | U)) = (fs_nil | V)) )

( fs_map_single : !! {U,V : Type}{f : (U -> V)}{x : U}
  ((fs_map f (fs_single x)) = (fs_single (f x))) )

( fs_map_union : !! {U,V : Type}{m,m' : (fs U)}{f : (U -> V)}
  (Not (fs_empty m)) -> (Not (fs_empty m')) ->
  ((fs_map f (fs_union m m')) = (fs_union (fs_map f m) (fs_map f m'))) )

--- 

( fs_select : {T | Type} (T -> Prop) -> (fs T) -> (fs T) )

( fs_select_nil : !! {T : Type}{P : (T -> Prop)}
  ((fs_select P (fs_nil | T)) = (fs_nil | T)) )

( fs_select_single_1 : !! {T : Type}{P : (T -> Prop)}{x : T}
  (P x) -> ((fs_select P (fs_single x)) = (fs_single x)) )

( fs_select_single_2 : !! {T : Type}{P : (T -> Prop)}{x : T}
  (Not (P x)) -> ((fs_select P (fs_single x)) = (fs_nil | T)) )

( fs_select_union : !! {T : Type}{m,m' : (fs T)}{P : (T -> Prop)}
  (Not (fs_empty m)) -> (Not (fs_empty m')) ->
  ((fs_select P (fs_union m m')) = (fs_union (fs_select P m) (fs_select P m'))) )

( fs_le_select : {T : Type}{m : (fs T)}{P : T -> Prop} 
  (fs_le (fs_select P m) m) )

( fs_in_select : {T : Type}{m : (fs T)}{P : (T -> Prop)}{x : T} 
  (fs_in (fs_select P m) x) -> (P x) )

---

( fs_multi : {T | Type} nat -> T -> (fs T) )

( fs_occ_multi_eq : {T : Type}{n : nat}{x : T}
  ((fs_occ (fs_multi n x) x) = n) )

( fs_occ_multi_neq : {T : Type}{n : nat}{x,y : T}
  (Not (x = y)) -> ((fs_occ (fs_multi n x) y) = 0) )

( done )