proposition: Lemma rCompSeval_sound n phi s l: Proc phi -> let (k,t) := rCompSeval n (l,s) in k >= l /\ denoteComp phi s >[(k-l)] denoteComp phi t.
proof: Proof. Proof with (repeat inv_validComp;repeat (eassumption || constructor || intuition idtac || lia || subst ; eauto using star || rewrite Nat.sub_diag in * || rewrite Nat.sub_0_r in *||cbn in * )). intros. unfold rCompSeval. pose (p:= (l,s)). change (let (k, t) := fst (rCompSeval' n p) in k >= fst p /\denoteComp phi (snd p) >[(k-(fst p))] denoteComp phi t). generalize p. clear l s p. intros p. functional induction (rCompSeval' n p); intros;cbn... - rewrite e2,e5 in *... eapply rCompBeta_sound in e8;try eauto. destruct (rCompSeval' _ (S _,_ ));destruct p... eapply (CPow_trans (t:= denoteComp phi (s' t')))... - rewrite e2,e5 in *... eapply (CPow_trans (t:= denoteComp phi (s' t')))... - rewrite e2,e5 in *... eapply (CPow_trans (t:= denoteComp phi (s' t')))... - rewrite e2,e5 in *... eapply (CPow_trans (t:= denoteComp phi (s' t')))... - rewrite <- map_nth... - repeat destruct (rCompSeval' _ _)... destruct p... eapply CPow_trans... Qed.
imports: Undecidability.L.Tactics(LClos) ZArith FunInd