proposition: Lemma wellBehaved_decompose {Tl T} : forall (t: ArithExpr Tl T) (l : evalExprTypeRounded_list Tl) md, wellBehaved t l md <-> wellDefined t l md /\ operationsExact t l md.
proof: Proof. induction t as [| | | Tl T OP | Tl OP | | | | | | | | Tl T | | | |]. - easy. - easy. - easy. - intros l md. now destruct OP; simpl; rewrite IHt1, IHt2; [| | | destruct T]. - intros l md. now destruct OP; simpl; rewrite IHt1, IHt2. - intros l md. simpl. now rewrite IHt1, IHt2, IHt3. - intros l md. simpl. now rewrite IHt1, IHt2, IHt3. - easy. - intros l md. simpl. now rewrite IHt. - intros l md. simpl. now rewrite IHt. - intros l md. simpl. now rewrite IHt. - intros l md. simpl. now rewrite IHt. - intros l md. simpl. now rewrite IHt. - intros l md. simpl. now rewrite IHt1, IHt2. - intros l md. simpl. now rewrite IHt. - easy. - easy. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)