def contains_row.go

minebender-game@1.0.0.0 · proof_cells.bend:160

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

160def contains_row.go(+y: Nat, +a: Nat, +t: List<&2, Nat>, +x: Nat, +b: Bool,
161  e: {Bool.or(b, memn(t, x)) == True{} : Bool}, be: {Nat.is_eq(a, x) == b : Bool},
162  ih: {memn(t, x) == True{} : Bool} -> {B.contains(B.row_cells(y, t), T.Pos{x, y}) == True{} : Bool}) ->
163  {Bool.or(B.same(T.Pos{a, y}, T.Pos{x, y}), B.contains(B.row_cells(y, t), T.Pos{x, y})) == True{} : Bool}:
164  match b:
165    case True{}:
166      %Equal.sym(Bool, Nat.is_eq(a, x), True{}, be) :
167        {Bool.or(Bool.and(_, Nat.is_eq(y, y)), B.contains(B.row_cells(y, t), T.Pos{x, y})) == True{} : Bool}
168      %Equal.sym(Bool, Nat.is_eq(y, y), True{}, P.eq_refl(y)) :
169        {Bool.or(Bool.and(True{}, _), B.contains(B.row_cells(y, t), T.Pos{x, y})) == True{} : Bool}
170      {==}
171    case False{}:
172      %Equal.sym(Bool, B.contains(B.row_cells(y, t), T.Pos{x, y}), True{}, ih(e)) :
173        {Bool.or(B.same(T.Pos{a, y}, T.Pos{x, y}), _) == True{} : Bool}
174      or_true_r(B.same(T.Pos{a, y}, T.Pos{x, y}))