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 begcd_mips_prelude_prg

Require Import mips_bipl.
Import mips_bipl.expr_m.
Require Import simu.
Require Import multi_is_even_prg.
Require Import multi_div2_prg.
Require Import multi_mul2_prg.
Require Import multi_is_even_and_prg.

Local Open Scope mips_cmd_scope.

Definition prelude_mips rk rg rx ry a0 a1 a2 a3 :=
  multi_is_even_and rk rx ry a0 a1;
  while.while (bne a0 r0) (
    (multi_div2 rk rx a0 a1 a2 a3 ;
     multi_div2 rk ry a0 a1 a2 a3 ;
     multi_mul2 rk rg a0 a1 a2 a3) ;
    multi_is_even_and rk rx ry a0 a1).