ProofGen.gen_left_firsts.go: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_gen.bend as ProofGen
Lines 599-615 of minebender-game@1.0.0.0/proof_gen.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_gen.bend&start_line=599&end_line=615

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

def gen_left_firsts.go(+z: G.Zone, +p: T.Pos, +t: List<&2, T.Pos>, +s: Bool,
  ih: {Nat.add(G.gen.left(z, t), outs(z, t)) == List.length(&2, T.Pos, t) : Nat}) ->
  {Nat.add(Nat.add(Bool.pick(Nat, s, 0n, 1n), G.gen.left(z, t)),
     Nat.add(Bool.pick(Nat, s, 1n, 0n), outs(z, t))) == 1n+List.length(&2, T.Pos, t) : Nat}:
  match s:
    case True{}:
      %Equal.sym(Nat, Nat.add(G.gen.left(z, t), 1n+outs(z, t)),
        1n+Nat.add(G.gen.left(z, t), outs(z, t)),
        P.add_succ(G.gen.left(z, t), outs(z, t))) :
        {_ == 1n+List.length(&2, T.Pos, t) : Nat}
      %Equal.sym(Nat, Nat.add(G.gen.left(z, t), outs(z, t)), List.length(&2, T.Pos, t), ih) :
        {1n+_ == 1n+List.length(&2, T.Pos, t) : Nat}
      {==}
    case False{}:
      %Equal.sym(Nat, Nat.add(G.gen.left(z, t), outs(z, t)), List.length(&2, T.Pos, t), ih) :
        {1n+_ == 1n+List.length(&2, T.Pos, t) : Nat}
      {==}

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.pick
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=Zone
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=gen.left
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_base.bend&name=add_succ
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_gen.bend&name=outs
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Pos