law Growth.maximum_monotone
gralha-bendquest@0.1.0.0 · growth.bend:125
import gralha-bendquest@0.1.0.0/growth.bend as Growth
import Base
import gralha-bendquest@0.1.0.0/game.bend as G
125law Growth.maximum_monotone:
126 for +level0: Nat
127 for +level1: Nat
128 for +vit0: Nat
129 for +vit1: Nat
130 for +bonus: U32
131 for +ceiling: U32
132 for +levels: {G.Bq.Nat.le(level0, level1) == True{} : Bool}
133 for +vitalities: {G.Bq.Nat.le(vit0, vit1) == True{} : Bool}
134 {G.Bq.Nat.le(U32.to_nat(Growth.maximum(level0, vit0, bonus, ceiling)), U32.to_nat(Growth.maximum(level1, vit1, bonus, ceiling))) == True{} : Bool}