proposition: Lemma step_star_fun_app_inv: forall sched s ls1 ls2 s'', step_star_fun nil sched s = Some (ls1 ++ ls2, s'')%list -> exists sched1 s' sched2, sched = (sched1 ++ sched2)%list /\ step_star_fun nil sched1 s = Some (ls1, s') /\ step_star_fun nil sched2 s' = Some (ls2, s'').
proof: Proof. Proof using. intros. clear max_nid_eq. revert s sched ls2 s'' H. induction ls1; simpl; intros. * exists nil; exists s; exists sched; simpl; split; auto. * apply step_star_fun_cons_inv in H. destruct H as [task[s'[sched'[Heq[Hs Hss]]]]]; subst sched. apply IHls1 in Hss. destruct Hss as [sched1[s'0[sched2[Heq[Hss1 Hss2]]]]]; subst sched'. exists (task::sched1)%list; exists s'0; exists sched2; simpl; split_all; auto. rewrite Hs. apply prefix_step_star_fun with (ls3:=[a]); auto. Qed.
imports: Coq(FunctionalExtensionality List Arith Lia) Chapar(Predefs KVStore)