Lvc.LivenessValidators

Require Import DecSolve IL Annotation Liveness TrueLiveness LengthEq.

Instance argsLive_dec Caller Callee Y Z
      : Computable (argsLive Caller Callee Y Z).

Definition live_sound_dec i Lv s slv (an:annotation s slv)
      : Computable (live_sound i Lv s slv).

Instance live_sound_dec_inst i Lv s slv `{Computable(annotation s slv)}
: Computable (live_sound i Lv s slv).

Definition true_live_sound_dec i Lv s slv (an:annotation s slv)
      : Computable (true_live_sound i Lv s slv).

Instance true_live_sound_dec_inst i Lv s slv `{Computable(annotation s slv)}
: Computable (true_live_sound i Lv s slv).