proposition: Lemma BSM_computable_iff {k} (R : Vector.t nat k -> nat -> Prop) : BSM_computable R <-> exists n : nat, exists i : nat, exists P : list (bsm_instr (1 + k + n)), (forall v : Vector.t nat k,forall m, R v m -> exists c v', BSM.eval (1 + k + n) (i, P) (i, (@List.nil bool :: Vector.map (fun n => List.repeat true n) v) ++ Vector.const (@List.nil bool) n) (c, List.repeat true m :: v')) /\ (forall v, sss.sss_terminates (@bsm_sss _) (i, P) (i, (@List.nil bool :: Vector.map (fun n => List.repeat true n) v) ++ Vector.const (@List.nil bool) n) -> exists m, R v m).
proof: Proof. split. - intros (n & i & P & H). exists n, i, P. split. + intros v m ? % H; eauto. + intros v [(c, v') H1]. pose proof (H2 := H1). eapply eval_iff in H2 as (m & v'' & H2) % H. subst. eapply eval_iff in H1. eexists. eapply H. eexists. eexists. eapply H1. - intros (n & i & P & H1 & H2). exists n, i, P. intros v. split. + intros m. split. * intros (c & v' & Hvm) % H1. fold plus in *. exists c, v'. eapply Hvm. * intros (c & v' & Hvm % eval_iff). fold plus in *. edestruct H2 as [m' H']. -- eexists. eassumption. -- enough (m' = m) as -> by assumption. eapply H1 in H' as (c' & v'' & H' % eval_iff). destruct Hvm as [Hvm1 Hvm2]. eapply sss.sss_compute_fun in Hvm1. 5: eapply H'. 3: eapply H'. 3: eapply Hvm2. 2: eapply bsm_sss_fun. inversion Hvm1. eapply (f_equal (@length bool)) in H3. now rewrite !repeat_length in H3. + intros c v' H % eval_iff. edestruct H2 as [m Hm]. { eexists. eauto. } eapply H1 in Hm as (c' & v'' & [Hm1 Hm2] % eval_iff). fold plus in *. exists m, v''. eapply sss.sss_compute_fun in Hm1. 5: eapply H. 3: eapply H. 3: eapply Hm2. 2: eapply bsm_sss_fun. inversion Hm1. congruence. Qed.
imports: Coq(List Vector)