def room_left.k

minebender-game@1.0.0.0 · proof_gen.bend:872

import Base
import minebender-game@1.0.0.0/LAWS.bend as L
import minebender-game@1.0.0.0/proof_base.bend as P

872# Room for n mines and 9 more among the L + O cells, with O <= 9: n <= L.
873def room_left.k(+l: Nat, +o: Nat, +m: Nat, +n: Nat, e: {Nat.add(l, o) == m : Nat},
874  wb: P.LeW(o, 9n), wr: P.LeW(Nat.add(n, 9n), m)) -> {Nat.is_le(n, l) == True{} : Bool}:
875  match wb:
876    case (+d, eb):
877      match wr:
878        case (+k, er):
879          +dk = Nat.add(d, k)
880          +t1 = Equal.trans(Nat, Nat.add(o, l), m, Nat.add(Nat.add(n, 9n), k),
881            Equal.trans(Nat, Nat.add(o, l), Nat.add(l, o), m, P.add_comm(o, l), e), er)
882          +t2 = Equal.cong(Nat, Nat, x => Nat.add(Nat.add(n, x), k), 9n, Nat.add(o, d), eb)
883          +t4 = Equal.cong(Nat, Nat, x => Nat.add(n, x), Nat.add(Nat.add(o, d), k), Nat.add(o, dk), P.add_assoc(o, d, k))
884          +t345 = Equal.trans(Nat, Nat.add(Nat.add(n, Nat.add(o, d)), k), Nat.add(n, Nat.add(Nat.add(o, d), k)),
885            Nat.add(o, Nat.add(n, dk)), P.add_assoc(n, Nat.add(o, d), k),
886            Equal.trans(Nat, Nat.add(n, Nat.add(Nat.add(o, d), k)), Nat.add(n, Nat.add(o, dk)), Nat.add(o, Nat.add(n, dk)),
887              t4, P.add_left_comm(n, o, dk)))
888          +e3 = Equal.trans(Nat, Nat.add(o, l), Nat.add(Nat.add(n, 9n), k), Nat.add(o, Nat.add(n, dk)), t1,
889            Equal.trans(Nat, Nat.add(Nat.add(n, 9n), k), Nat.add(Nat.add(n, Nat.add(o, d)), k), Nat.add(o, Nat.add(n, dk)),
890              t2, t345))
891          %Equal.sym(Nat, l, Nat.add(n, dk), add_cancel_l(o, l, Nat.add(n, dk), e3)) : {Nat.is_le(n, _) == True{} : Bool}
892          P.le_of_add(n, dk)