include "ERTL/ERTL.ma".
include "utilities/BitVectorTrieSet.ma".

definition VariableSet ≝ (BitVectorTrieSet 16) × (BitVectorTrieSet 16).

definition VariableProperty ≝ (BitVectorTrieSet 16) × (BitVectorTrieSet 16).

definition vs_bottom ≝ 〈set_empty 16, set_empty 16〉.

definition vs_p_singleton ≝
  λar: AbstractRegister.
  match ar with [
  mkAbstractRegister r ⇒ 〈set_singleton ? r, set_empty 16〉
  ].
  
definition vs_h_singleton ≝
  λr: Register.
  let index ≝ word_of_register r in
    〈set_empty 16, set_singleton ? index〉.
    
definition join: VariableSet → VariableSet → VariableSet ≝
  λvs1: VariableSet.
  λvs2: VariableSet.
    〈set_union ? (\fst vs1) (\fst vs2), set_union ? (\snd vs1) (\snd vs2)〉.
    
definition vs_is_maximal ≝ λA: Type[0]. λa: A. false.

definition vs_eq: VariableSet → VariableSet → bool ≝
  λvs1: VariableSet.
  λvs2: VariableSet.
    andb (set_eq ? (\fst vs1) (\fst vs2)) (set_eq ? (\snd vs1) (\snd vs2)).
    
definition vs_diff: VariableSet → VariableSet → VariableSet ≝
  λvs1: VariableSet.
  λvs2: VariableSet.
    〈set_diff ? (\fst vs1) (\fst vs2), set_diff ? (\snd vs1) (\snd vs2)〉.