proposition: Lemma mu_queens_state_nondeter n : mu_queens n = protect (put (0, [::], [::])%Z >> queensBody (map Z_of_nat (iota 0 n))).
proof: Proof. rewrite mu_queensE. transitivity (perms (map Z.of_nat (iota 0 n)) >>= (fun xs => protect (put (0, [::], [::])%Z >> foldr opdot_queens (Ret [::]) xs))). bind_ext => s /=. exact: corollary45. transitivity (protect (put (0, [::], [::])%Z >> perms (map Z.of_nat (iota 0 n)) >>= foldr opdot_queens (Ret [::]))). rewrite -getpermsC /protect; bind_ext => s. rewrite !bindA putpermsC. by under eq_bind do rewrite bindA. rewrite /protect; bind_ext => st. by rewrite !bindA. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monae_lib hierarchy monad_lib fail_lib state_lib