def gen_left_firsts.go

minebender-game@1.0.0.0 · proof_gen.bend:599

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/game.bend as G
import minebender-game@1.0.0.0/proof_base.bend as P

599def gen_left_firsts.go(+z: G.Zone, +p: T.Pos, +t: List<&2, T.Pos>, +s: Bool,
600  ih: {Nat.add(G.gen.left(z, t), outs(z, t)) == List.length(&2, T.Pos, t) : Nat}) ->
601  {Nat.add(Nat.add(Bool.pick(Nat, s, 0n, 1n), G.gen.left(z, t)),
602     Nat.add(Bool.pick(Nat, s, 1n, 0n), outs(z, t))) == 1n+List.length(&2, T.Pos, t) : Nat}:
603  match s:
604    case True{}:
605      %Equal.sym(Nat, Nat.add(G.gen.left(z, t), 1n+outs(z, t)),
606        1n+Nat.add(G.gen.left(z, t), outs(z, t)),
607        P.add_succ(G.gen.left(z, t), outs(z, t))) :
608        {_ == 1n+List.length(&2, T.Pos, t) : Nat}
609      %Equal.sym(Nat, Nat.add(G.gen.left(z, t), outs(z, t)), List.length(&2, T.Pos, t), ih) :
610        {1n+_ == 1n+List.length(&2, T.Pos, t) : Nat}
611      {==}
612    case False{}:
613      %Equal.sym(Nat, Nat.add(G.gen.left(z, t), outs(z, t)), List.length(&2, T.Pos, t), ih) :
614        {1n+_ == 1n+List.length(&2, T.Pos, t) : Nat}
615      {==}