proposition: Theorem last_def : forall b pc, last b = Some pc -> next b pc = None.
proof: Proof. intros block pc0 Hlast. unfold last in Hlast. destruct (lastS (statements block)). destruct s. inversion Hlast; clear Hlast. unfold next. rewrite H0. destruct (suffixS (statements block) pc0). destruct s; destruct s. destruct a. destruct H1. assert (Last x x0). elim H; intros p Heq. rewrite <- Heq in l. apply Last_app_inv with (l1 := p). intro Hnil. rewrite Hnil in H1; discriminate H1. assumption. rewrite <- H0 in H2. apply PC_unique_impl with (b := block) in H2. rewrite H2 in H1. assert (x0 = x::nil). apply Last_head_singleton with (b := block); assumption. rewrite H4; reflexivity. apply Suffix_In with (s := x0). assumption. apply In_head; assumption. apply Suffix_In with (s := x0). assumption. apply Last_In; assumption. reflexivity. discriminate Hlast. Qed.
imports: JML(JMLProgramPlus) Coq(ZArith) JML(ZHelpers) JML(LogicHelpers) Coq(Bool) Coq(Sumbool) Coq(Ndec) JML(PosAux) JML(EqBoolAux) Coq(Relation_Operators) Coq(List) JML(ListFunctions) JML(ListHelpers) JML(OptionHelpers)