Type Neighbours is
Imports
  ref: BOOLEAN
  ref: INTEGER
  ref: STRING

Sorts
  new element
  new line
  new neighbours

Operators
  ctor: _1 : -> element
  ctor: _2 : -> element
  ctor: _3 : -> element
  ctor: _4 : -> element
  ctor: __ : -> element
  ctor: x : -> element

  oper: mkline : element element element element element element element -> line
  oper: mkpuzzle : line line line line line line line -> neighbours
  oper: columns : neighbours -> neighbours
  oper: testelem : element element -> Bool
  oper: testelemX : element element element -> Bool
  oper: testline : line -> Bool
  oper: testlineX : line -> Bool
  oper: testpuzzlelines : neighbours -> Bool
  oper: testpuzzlelinesX : neighbours -> Bool
  oper: testpuzzle : neighbours -> Bool
  oper: elemToInt : element -> Int
  oper: boardWrittenValid : element element element -> String

Variables
  var p : neighbours

  var vl1 : line
  var nl1 : line
  var vl2 : line
  var nl2 : line
  var vl3 : line
  var nl3 : line
  var vl4 : line

  var e1 : element
  var n1 : element
  var e2 : element
  var n2 : element
  var e3 : element
  var n3 : element
  var e4 : element

  var e11 : element
  var e12 : element
  var e13 : element
  var e14 : element
  var e15 : element
  var e16 : element
  var e17 : element
  var e21 : element
  var e22 : element
  var e23 : element
  var e24 : element
  var e25 : element
  var e26 : element
  var e27 : element
  var e31 : element
  var e32 : element
  var e33 : element
  var e34 : element
  var e35 : element
  var e36 : element
  var e37 : element
  var e41 : element
  var e42 : element
  var e43 : element
  var e44 : element
  var e45 : element
  var e46 : element
  var e47 : element
  var e51 : element
  var e52 : element
  var e53 : element
  var e54 : element
  var e55 : element
  var e56 : element
  var e57 : element
  var e61 : element
  var e62 : element
  var e63 : element
  var e64 : element
  var e65 : element
  var e66 : element
  var e67 : element
  var e71 : element
  var e72 : element
  var e73 : element
  var e74 : element
  var e75 : element
  var e76 : element
  var e77 : element
Axioms
  axiom: elemToInt(_1()) = 1
  axiom: elemToInt(_2()) = 2
  axiom: elemToInt(_3()) = 3
  axiom: elemToInt(_4()) = 4

  axiom: columns(mkpuzzle(mkline(:e11, :e12, :e13, :e14, :e15, :e16, :e17), mkline(:e21, :e22, :e23, :e24, :e25, :e26, :e27), mkline(:e31, :e32, :e33, :e34, :e35, :e36, :e37), mkline(:e41, :e42, :e43, :e44, :e45, :e46, :e47), mkline(:e51, :e52, :e53, :e54, :e55, :e56, :e57), mkline(:e61, :e62, :e63, :e64, :e65, :e66, :e67), mkline(:e71, :e72, :e73, :e74, :e75, :e76, :e77))) = mkpuzzle(mkline(:e11, :e21, :e31, :e41, :e51, :e61, :e71), mkline(:e12, :e22, :e32, :e42, :e52, :e62, :e72), mkline(:e13, :e23, :e33, :e43, :e53, :e62, :e73), mkline(:e14, :e24, :e34, :e44, :e54, :e64, :e74), mkline(:e15, :e25, :e35, :e45, :e55, :e65, :e75), mkline(:e16, :e26, :e36, :e46, :e56, :e66, :e76), mkline(:e17, :e27, :e37, :e47, :e57, :e67, :e77))

  axiom: testelem(:e1, :n1) = Or(Equal(:e1, __()), Or(Equal(:n1, __()), Not(Equal(:e1, :n1))))

  axiom: testline(mkline(:e1, :n1, :e2, :n2, :e3, :n3, :e4)) = And(testelem(:e1, :e2), And(testelem(:e1, :e3), And(testelem(:e1, :e4), And(testelem(:e2, :e3), And(testelem(:e2, :e4), testelem(:e3, :e4))))))

  axiom: testpuzzlelines(mkpuzzle(:vl1, :nl1, :vl2, :nl2, :vl3, :nl3, :vl4)) = And(testline(:vl1), And(testline(:vl2), And(testline(:vl3), testline(:vl4))))

  axiom: testelemX(:e1, :n1, :e2) = If_Then_Else(Equal(:n1, x()), Or(Equal(SUB(elemToInt(:e1), 1), elemToInt(:e2)), Or(Equal(SUB(elemToInt(:e2), 1), elemToInt(:e1)), Or(Equal(:e1, __()), Equal(:e2, __())))), Not(Or(Equal(SUB(elemToInt(:e1), 1), elemToInt(:e2)), Equal(SUB(elemToInt(:e2), 1), elemToInt(:e1)))))

  axiom: boardWrittenValid(:e1, :n1, :e2) = If_Then_Else(Or(Equal(elemToInt(:n1), 1), Or(Equal(elemToInt(:n1), 2), Or(Equal(elemToInt(:n1), 3), Equal(elemToInt(:n1), 4)))), "Board is written in unvalid", "Board is written in valid")

  axiom: testlineX(mkline(:e1, :n1, :e2, :n2, :e3, :n3, :e4)) = And(testelemX(:e1, :n1, :e2), And(testelemX(:e2, :n2, :e3), testelemX(:e3, :n3, :e4)))

  axiom: testpuzzlelinesX(mkpuzzle(:vl1, :nl1, :vl2, :nl2, :vl3, :nl3, :vl4)) = And(testlineX(:vl1), And(testlineX(:vl2), And(testlineX(:vl3), testlineX(:vl4))))

  axiom: testpuzzle(:p) = And(testpuzzlelines(:p), And(testpuzzlelines(columns(:p)), And(testpuzzlelinesX(:p), testpuzzlelinesX(columns(:p)))))

Reductions
  reduce : columns(mkpuzzle(mkline(_1(), _1(), _2(), __(), _3(), x(), _4()), mkline(x(), __(), __(), __(), __(), __(), __()), mkline(_1(), __(), _2(), __(), _3(), x(), _4()), mkline(__(), __(), __(), __(), __(), __(), __()), mkline(_1(), __(), _2(), __(), _3(), x(), _4()), mkline(__(), __(), __(), __(), __(), __(), __()), mkline(_1(), __(), _2(), __(), _3(), x(), _4())))

  reduce : testelem(_1(), _2())
  reduce : testelem(_2(), _1())
  reduce : testelem(_2(), _2())

  reduce : testline(mkline(_1(), __(), _2(), __(), _3(), x(), _2()))

  reduce : testpuzzlelines(mkpuzzle(mkline(_1(), _1(), _2(), __(), _3(), x(), _4()), mkline(x(), __(), __(), __(), __(), __(), __()), mkline(_1(), __(), _2(), __(), _3(), x(), _4()), mkline(__(), __(), __(), __(), __(), __(), __()), mkline(_1(), __(), _2(), __(), _3(), x(), _4()), mkline(__(), __(), __(), __(), __(), __(), __()), mkline(_1(), __(), _2(), __(), _3(), x(), _4())))
  reduce : testelemX(_1(), x(), _2())
  reduce : testelemX(_2(), x(), _1())
  reduce : testelemX(_1(), __(), _2())
  reduce : testelemX(_2(), __(), _1())
  reduce : testelemX(_1(), x(), _3())
  reduce : testelemX(_3(), x(), _1())
  reduce : testelemX(_1(), __(), _3())
  reduce : testelemX(_3(), __(), _1())

  reduce : testlineX(mkline(_1(), __(), _2(), __(), _3(), x(), _2()))

  reduce : testpuzzlelinesX(mkpuzzle(mkline(_1(), _1(), _2(), __(), _3(), x(), _4()), mkline(x(), __(), __(), __(), __(), __(), __()), mkline(_1(), __(), _2(), __(), _3(), x(), _4()), mkline(__(), __(), __(), __(), __(), __(), __()), mkline(_1(), __(), _2(), __(), _3(), x(), _4()), mkline(__(), __(), __(), __(), __(), __(), __()), mkline(_1(), __(), _2(), __(), _3(), x(), _4())))
  reduce : testpuzzle(mkpuzzle(mkline(_4(), __(), _2(), x(), _3(), __(), _1()), mkline(__(), __(), x(), __(), x(), __(), __()), mkline(_1(), __(), _3(), x(), _2(), __(), _4()), mkline(x(), __(), x(), __(), x(), __(), x()), mkline(_2(), __(), _4(), __(), _1(), __(), _3()), mkline(x(), __(), __(), __(), __(), __(), x()), mkline(_3(), __(), _1(), __(), _4(), __(), _2())))
  reduce : testpuzzle(mkpuzzle(mkline(_4(), __(), __(), x(), __(), x(), __()), mkline(x(), __(), x(), __(), x(), __(), x()), mkline(__(), x(), __(), x(), __(), __(), _4()), mkline(__(), __(), __(), __(), __(), __(), __()), mkline(__(), __(), __(), x(), __(), x(), __()), mkline(x(), x(), x(), x(), x(), x(), x()), mkline(__(), x(), __(), x(), __(), __(), __())))
  reduce : testpuzzle(mkpuzzle(mkline(_4(), __(), __(), x(), __(), x(), __()), mkline(x(), __(), x(), __(), x(), __(), x()), mkline(__(), x(), __(), x(), __(), __(), _4()), mkline(__(), __(), __(), __(), __(), __(), __()), mkline(__(), __(), _1(), x(), _2(), x(), _3()), mkline(x(), x(), x(), x(), x(), x(), x()), mkline(_1(), x(), _2(), x(), _3(), __(), __())))
  reduce : If_Then_Else(Or(Equal(elemToInt(_1()), 1), Or(Equal(elemToInt(_1()), 2), Or(Equal(elemToInt(_1()), 3), Equal(elemToInt(_1()), 4)))), "Board is written unvalid", "Board is written valid")
  reduce : boardWrittenValid(_1(), _1(), _2())