NB: This Coq documentation contains a revised version of the Coq implementation of these papers [1], [2], [3], [4], and is also the support for ongoing research. A partial archive (14/01/2001) is available at here. Drop us a line if you are interested in a complete, up-to-date archive.

Library multi_is_even_and_prg

Require Import multi_is_even_prg.
Require Import simu.

Local Open Scope mips_cmd_scope.

Definition multi_is_even_and rk rx ry a0 a1 :=
multi_is_even rk rx a0 ; multi_is_even rk ry a1 ; cmd_and a0 a0 a1.