Game.Bq.buy_burns_exact_gold: law of gralha-bendquest@0.1.0.0
Import: import gralha-bendquest@0.1.0.0/game.bend as Game
Lines 950-951 of gralha-bendquest@0.1.0.0/game.bend: https://jend.leeeet.dev/read.txt?path=gralha-bendquest@0.1.0.0/game.bend&start_line=950&end_line=951

import Base

law Bq.buy_burns_exact_gold:
  (@+k_0: Nat -> (@+h_1: Bq.Hero -> (@+__2: {Bq.buy_ok(k_0, h_1) == True{} : Bool} -> {Bq.Nat.add(Bq.iprice(k_0), Bq.hero_gold(Bq.hero_step(Bq.HOp.Buy{k_0}, h_1))) == Bq.hero_gold(h_1) : Nat})))

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Bool.and_r
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.HOp
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Hero
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Info
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Nat.add
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Nat.add_sub_cancel
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Nat.le
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.Nat.lt
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.buy_ok
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.hero_gold
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.hero_step
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.hero_step_go
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.iprice
  https://jend.leeeet.dev/definition.txt?path=gralha-bendquest@0.1.0.0/game.bend&name=Bq.item_info