fact: Record state : Set := mkstate {state_n : nat; state_p : nat; state_b : bool}.
imports: Arith Peano_dec Constants Mult_compl Wf_nat euclid Le_lt_compl Euclid shift Compare_dec imperative while two_power log2_spec