law inv_of
minebender-game@1.0.0.0 · proof_laws.bend:477
import minebender-game@1.0.0.0/proof_laws.bend as ProofLaws
import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/game.bend as G
import minebender-game@1.0.0.0/LAWS.bend as L
import minebender-game@1.0.0.0/proof_inv.bend as PI
477law inv_of:
478 for +w: Nat
479 for +h: Nat
480 for +layout: T.Grid(Bool)
481 for +g: G.Game
482 for +acts: List<&2, T.Action>
483 for +e: {L.play(acts, G.fresh(w, h, layout)) == g : G.Game}
484 PI.Inv(w, h, layout, g)