From Undecidability.Shared Require Import DLW.Vec.vec DLW.Vec.pos.
From Undecidability.MuRec Require Import recalg.

Set Implicit Arguments.

Reserved Notation " '[' f ';' v ']' '~~>' x " (at level 70).


Inductive ra_bs : forall k, recalg k -> vec nat k -> nat -> Prop :=
    | in_ra_bs_cst : forall n v, [ra_cst n; v] ~~> n
    | in_ra_bs_zero : forall v, [ra_zero; v] ~~> 0
    | in_ra_bs_succ : forall v, [ra_succ; v] ~~> S (vec_head v)
    | in_ra_bs_proj : forall k v j, [@ra_proj k j; v] ~~> vec_pos v j
    
    | in_ra_bs_comp : forall k i f (gj : vec (recalg i) k) v w x,
                                   (forall j, [vec_pos gj j; v] ~~> vec_pos w j)
                               -> [f; w] ~~> x
                               -> [ra_comp f gj; v] ~~> x

    | in_ra_bs_rec_0 : forall k f (g : recalg (S (S k))) v x,
                                              [f; v] ~~> x
                               -> [ra_rec f g; 0##v] ~~> x

    | in_ra_bs_rec_S : forall k f (g : recalg (S (S k))) v n x y,
                                              [ra_rec f g; n##v] ~~> x
                               -> [g; n##x##v] ~~> y
                               -> [ra_rec f g; S n##v] ~~> y
                               
    | in_ra_bs_min : forall k (f : recalg (S k)) v x w ,
                           (forall j : pos x, [f; pos2nat j##v] ~~> S (vec_pos w j))
                               -> [f; x##v] ~~> 0
                               -> [ra_min f; v] ~~> x
where " [ f ; v ] ~~> x " := (@ra_bs _ f v x).