def firsts_row.end

minebender-game@1.0.0.0 · proof_gen.bend:716

import Base

716def firsts_row.end(+a: Bool, +b: Bool, +c: Nat) ->
717  {Nat.add(Bool.pick(Nat, Bool.and(a, b), 1n, 0n), Bool.pick(Nat, b, c, 0n))
718    == Bool.pick(Nat, b, Nat.add(Bool.pick(Nat, a, 1n, 0n), c), 0n) : Nat}:
719  match a b:
720    case True{} True{}:
721      {==}
722    case True{} False{}:
723      {==}
724    case False{} True{}:
725      {==}
726    case False{} False{}:
727      {==}