law Health.hurt_word_preserves_bound

gralha-bendquest@0.1.0.0 · health.bend:399

import Base
import gralha-bendquest@0.1.0.0/game.bend as G

399law Health.hurt_word_preserves_bound:
400  for +hp: U32
401  for +damage: U32
402  for +maximum: U32
403  for +valid: {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(maximum)) == True{} : Bool}
404  {G.Bq.Nat.le(U32.to_nat(Health.hurt_word(hp, damage)), U32.to_nat(maximum)) == True{} : Bool}