Class:
Navigation:
 0-0     
Instance:
Relationship:
Domain:
Links:
Automated Pattern Deduction for Connect 4 in 1 Move (version 0.128 2024-12-20)

Step 0. Initial
 
game.connects4InMoves(player, 1) = true
Step 1. The system substitutes game.connects4InMoves(player, 1) with its predefined equivalence definition <=>
 
Ǝ xMove: (Start Exists Move Concept)
  xMove >= 0 and 
  xMove < xMax:
  game.afterMove(xMove).connects4InMoves(player, 0) = true
Ǝend xMove (End Exists Move Concept) and 
game.toMove = player and 
game.matrix.pppp(opponent(player)) = false
Step 2. The system substitutes connects4InMoves(player, 0) with its predefined equivalence definition <=>
 
Ǝ xMove: (Start Exists Move Concept)
  xMove >= 0 and 
  xMove < xMax:
  game.afterMove(xMove).matrix.pppp(player) = true and 
  game.afterMove(xMove).toMove = opponent(player)
Ǝend xMove (End Exists Move Concept) and 
game.toMove = player and 
game.matrix.pppp(opponent(player)) = false
Step 3. The system substitutes pppp(player) with its predefined equivalence definition <=>
 
Ǝ xMove: (Start Exists Move Concept)
  xMove >= 0 and 
  xMove < xMax:
  (Ǝ x0, y0: (Start Vertical Pattern with bottom coordinates x0, y0)
    x0 >= 0 and 
    x0 < xMax and 
    y0 >= 0 and 
    y0 < yMax - conn:
    ∀ extent: (Start All Extent: Connect in a Vertical Row Pattern)
      extent >= 0 and 
      extent < conn:
      game.afterMove(xMove).matrix(x0, y0 + extent) = player
    ∀end extent (End All Extent: Connect in a Vertical Row Pattern) and 
    game.afterMove(xMove).matrix.yEmpty(x0) = y0 + conn
  Ǝend x0, y0 (End Vertical Pattern with bottom coordinates x0, y0) or 
  Ǝ x0, y0: (Start Horizontal Pattern with left coordinates x0, y0)
    x0 >= 0 and 
    x0 < xMax - conn and 
    y0 >= 0 and 
    y0 < yMax:
    ∀ extent: (Start All Extent: Connect in a Horizontal Row Pattern)
      extent >= 0 and 
      extent < conn:
      game.afterMove(xMove).matrix(x0 + extent, y0) = player
    ∀end extent (End All Extent: Connect in a Horizontal Row Pattern) and 
    Ǝ pmEx: (Start Exists Previous Move Extent with Empty Position Above)
      pmEx >= 0 and 
      pmEx < conn:
      game.afterMove(xMove).matrix.yEmpty(x0 + pmEx) = y0 + 1
    Ǝend pmEx (End Exists Previous Move Extent with Empty Position Above)
  Ǝend x0, y0 (End Horizontal Pattern with left coordinates x0, y0) or 
  Ǝ x0, y0: (Start Diagonal Up Pattern with bottom-left coordinates x0, y0)
    x0 >= 0 and 
    x0 < xMax - conn and 
    y0 >= 0 and 
    y0 < yMax - conn:
    ∀ extent: (Start All Extent: Connect in a Diagonal Up Row Pattern)
      extent >= 0 and 
      extent < conn:
      game.afterMove(xMove).matrix(x0 + extent, y0 + extent) = player
    ∀end extent (End All Extent: Connect in a Diagonal Up Row Pattern) and 
    Ǝ pmEx: (Start Exists Previous Move Extent with Empty Position Above)
      pmEx >= 0 and 
      pmEx < conn:
      game.afterMove(xMove).matrix.yEmpty(x0 + pmEx) = y0 + pmEx + 1
    Ǝend pmEx (End Exists Previous Move Extent with Empty Position Above)
  Ǝend x0, y0 (End Diagonal Up Pattern with bottom-left coordinates x0, y0) or 
  Ǝ x0, y0: (Start Diagonal Down Pattern with top-left coordinates x0, y0)
    x0 >= 0 and 
    x0 < xMax - conn and 
    y0 >= conn and 
    y0 < yMax:
    ∀ extent: (Start All Extent: Connect in a Diagonal Down Row Pattern)
      extent >= 0 and 
      extent < conn:
      game.afterMove(xMove).matrix(x0 + extent, y0 - extent) = player
    ∀end extent (End All Extent: Connect in a Diagonal Down Row Pattern) and 
    Ǝ pmEx: (Start Exists Previous Move Extent with Empty Position Above)
      pmEx >= 0 and 
      pmEx < conn:
      game.afterMove(xMove).matrix.yEmpty(x0 + pmEx) = y0 - pmEx + 1
    Ǝend pmEx (End Exists Previous Move Extent with Empty Position Above)
  Ǝend x0, y0 (End Diagonal Down Pattern with top-left coordinates x0, y0)) and 
  game.afterMove(xMove).toMove = opponent(player)
Ǝend xMove (End Exists Move Concept) and 
game.toMove = player and 
game.matrix.pppp(opponent(player)) = false
Step 4. The system adds the game.afterMove(xMove) predefined function its equivalence definition <=>
 
Ǝ xMove: (Start Exists Move Concept)
  xMove >= 0 and 
  xMove < xMax:
  (Ǝ x0, y0: (Start Vertical Pattern with bottom coordinates x0, y0)
    x0 >= 0 and 
    x0 < xMax and 
    y0 >= 0 and 
    y0 < yMax - conn:
    ∀ extent: (Start All Extent: Connect in a Vertical Row Pattern)
      extent >= 0 and 
      extent < conn:
      game.afterMove(xMove).matrix(x0, y0 + extent) = player
    ∀end extent (End All Extent: Connect in a Vertical Row Pattern) and 
    game.afterMove(xMove).matrix.yEmpty(x0) = y0 + conn and 
    game.matrix.yEmpty(xMove) < yMax - 1 and 
    game.afterMove(xMove).toMove = opponent(game.toMove) and 
    game.afterMove(xMove).matrix(xMove, game.matrix.yEmpty(xMove)) = game.toMove and 
    game.afterMove(xMove).matrix.yEmpty(xMove) = game.matrix.yEmpty(xMove) + 1 and 
    ∀ x, y: (Start Matrix after move equals matrix before move except the new Disk)
      x >= 0 and 
      x < xMax and 
      y >= 0 and 
      y < yMax and 
      (x != xMove or 
      y != game.matrix.yEmpty(xMove)):
      game.afterMove(xMove).matrix(x, y) = game.matrix(x, y)
    ∀end x, y (End Matrix after move equals matrix before move except the new Disk)
  Ǝend x0, y0 (End Vertical Pattern with bottom coordinates x0, y0) or 
  Ǝ x0, y0: (Start Horizontal Pattern with left coordinates x0, y0)
    x0 >= 0 and 
    x0 < xMax - conn and 
    y0 >= 0 and 
    y0 < yMax:
    ∀ extent: (Start All Extent: Connect in a Horizontal Row Pattern)
      extent >= 0 and 
      extent < conn:
      game.afterMove(xMove).matrix(x0 + extent, y0) = player
    ∀end extent (End All Extent: Connect in a Horizontal Row Pattern) and 
    Ǝ pmEx: (Start Exists Previous Move Extent with Empty Position Above)
      pmEx >= 0 and 
      pmEx < conn:
      game.afterMove(xMove).matrix.yEmpty(x0 + pmEx) = y0 + 1
    Ǝend pmEx (End Exists Previous Move Extent with Empty Position Above) and 
    game.matrix.yEmpty(xMove) < yMax - 1 and 
    game.afterMove(xMove).toMove = opponent(game.toMove) and 
    game.afterMove(xMove).matrix(xMove, game.matrix.yEmpty(xMove)) = game.toMove and 
    game.afterMove(xMove).matrix.yEmpty(xMove) = game.matrix.yEmpty(xMove) + 1 and 
    ∀ x, y: (Start Matrix after move equals matrix before move except the new Disk)
      x >= 0 and 
      x < xMax and 
      y >= 0 and 
      y < yMax and 
      (x != xMove or 
      y != game.matrix.yEmpty(xMove)):
      game.afterMove(xMove).matrix(x, y) = game.matrix(x, y)
    ∀end x, y (End Matrix after move equals matrix before move except the new Disk)
  Ǝend x0, y0 (End Horizontal Pattern with left coordinates x0, y0) or 
  Ǝ x0, y0: (Start Diagonal Up Pattern with bottom-left coordinates x0, y0)
    x0 >= 0 and 
    x0 < xMax - conn and 
    y0 >= 0 and 
    y0 < yMax - conn:
    ∀ extent: (Start All Extent: Connect in a Diagonal Up Row Pattern)
      extent >= 0 and 
      extent < conn:
      game.afterMove(xMove).matrix(x0 + extent, y0 + extent) = player
    ∀end extent (End All Extent: Connect in a Diagonal Up Row Pattern) and 
    Ǝ pmEx: (Start Exists Previous Move Extent with Empty Position Above)
      pmEx >= 0 and 
      pmEx < conn:
      game.afterMove(xMove).matrix.yEmpty(x0 + pmEx) = y0 + pmEx + 1
    Ǝend pmEx (End Exists Previous Move Extent with Empty Position Above) and 
    game.matrix.yEmpty(xMove) < yMax - 1 and 
    game.afterMove(xMove).toMove = opponent(game.toMove) and 
    game.afterMove(xMove).matrix(xMove, game.matrix.yEmpty(xMove)) = game.toMove and 
    game.afterMove(xMove).matrix.yEmpty(xMove) = game.matrix.yEmpty(xMove) + 1 and 
    ∀ x, y: (Start Matrix after move equals matrix before move except the new Disk)
      x >= 0 and 
      x < xMax and 
      y >= 0 and 
      y < yMax and 
      (x != xMove or 
      y != game.matrix.yEmpty(xMove)):
      game.afterMove(xMove).matrix(x, y) = game.matrix(x, y)
    ∀end x, y (End Matrix after move equals matrix before move except the new Disk)
  Ǝend x0, y0 (End Diagonal Up Pattern with bottom-left coordinates x0, y0) or 
  Ǝ x0, y0: (Start Diagonal Down Pattern with top-left coordinates x0, y0)
    x0 >= 0 and 
    x0 < xMax - conn and 
    y0 >= conn and 
    y0 < yMax:
    ∀ extent: (Start All Extent: Connect in a Diagonal Down Row Pattern)
      extent >= 0 and 
      extent < conn:
      game.afterMove(xMove).matrix(x0 + extent, y0 - extent) = player
    ∀end extent (End All Extent: Connect in a Diagonal Down Row Pattern) and 
    Ǝ pmEx: (Start Exists Previous Move Extent with Empty Position Above)
      pmEx >= 0 and 
      pmEx < conn:
      game.afterMove(xMove).matrix.yEmpty(x0 + pmEx) = y0 - pmEx + 1
    Ǝend pmEx (End Exists Previous Move Extent with Empty Position Above) and 
    game.matrix.yEmpty(xMove) < yMax - 1 and 
    game.afterMove(xMove).toMove = opponent(game.toMove) and 
    game.afterMove(xMove).matrix(xMove, game.matrix.yEmpty(xMove)) = game.toMove and 
    game.afterMove(xMove).matrix.yEmpty(xMove) = game.matrix.yEmpty(xMove) + 1 and 
    ∀ x, y: (Start Matrix after move equals matrix before move except the new Disk)
      x >= 0 and 
      x < xMax and 
      y >= 0 and 
      y < yMax and 
      (x != xMove or 
      y != game.matrix.yEmpty(xMove)):
      game.afterMove(xMove).matrix(x, y) = game.matrix(x, y)
    ∀end x, y (End Matrix after move equals matrix before move except the new Disk)
  Ǝend x0, y0 (End Diagonal Down Pattern with top-left coordinates x0, y0)) and 
  game.afterMove(xMove).toMove = opponent(player)
Ǝend xMove (End Exists Move Concept) and 
game.toMove = player and 
game.matrix.pppp(opponent(player)) = false
Step 5. The system substitutes xMove with x0 in the first (vertical) pattern Ǝ x0, y0 and with x0 + pmEx in the horizontal, diagonal up and down patterns Ǝ x0, y0. <=>
 
Ǝ xMove: (Start Exists Move Concept)
  xMove >= 0 and 
  xMove < xMax:
  (Ǝ x0, y0: (Start Vertical Pattern with bottom coordinates x0, y0)
    x0 >= 0 and 
    x0 < xMax and 
    y0 >= 0 and 
    y0 < yMax - conn:
    ∀ extent: (Start All Extent: Connect in a Vertical Row Pattern)
      extent >= 0 and 
      extent < conn:
      game.afterMove(x0).matrix(x0, y0 + extent) = player
    ∀end extent (End All Extent: Connect in a Vertical Row Pattern) and 
    game.afterMove(x0).matrix.yEmpty(x0) = y0 + conn and 
    game.matrix.yEmpty(x0) < yMax - 1 and 
    game.afterMove(x0).toMove = opponent(game.toMove) and 
    game.afterMove(x0).matrix(x0, game.matrix.yEmpty(x0)) = game.toMove and 
    game.afterMove(x0).matrix.yEmpty(x0) = game.matrix.yEmpty(x0) + 1 and 
    ∀ x, y: (Start Matrix after move equals matrix before move except the new Disk)
      x >= 0 and 
      x < xMax and 
      y >= 0 and 
      y < yMax and 
      (x != x0 or 
      y != game.matrix.yEmpty(x0)):
      game.afterMove(x0).matrix(x, y) = game.matrix(x, y)
    ∀end x, y (End Matrix after move equals matrix before move except the new Disk)
  Ǝend x0, y0 (End Vertical Pattern with bottom coordinates x0, y0) or 
  Ǝ x0, y0: (Start Horizontal Pattern with left coordinates x0, y0)
    x0 >= 0 and 
    x0 < xMax - conn and 
    y0 >= 0 and 
    y0 < yMax:
    ∀ extent: (Start All Extent: Connect in a Horizontal Row Pattern)
      extent >= 0 and 
      extent < conn:
      game.afterMove(x0 + pmEx).matrix(x0 + extent, y0) = player
    ∀end extent (End All Extent: Connect in a Horizontal Row Pattern) and 
    Ǝ pmEx: (Start Exists Previous Move Extent with Empty Position Above)
      pmEx >= 0 and 
      pmEx < conn:
      game.afterMove(x0 + pmEx).matrix.yEmpty(x0 + pmEx) = y0 + 1
    Ǝend pmEx (End Exists Previous Move Extent with Empty Position Above) and 
    game.matrix.yEmpty(x0 + pmEx) < yMax - 1 and 
    game.afterMove(x0 + pmEx).toMove = opponent(game.toMove) and 
    game.afterMove(x0 + pmEx).matrix(x0 + pmEx, game.matrix.yEmpty(x0 + pmEx)) = game.toMove and 
    game.afterMove(x0 + pmEx).matrix.yEmpty(x0 + pmEx) = game.matrix.yEmpty(x0 + pmEx) + 1 and 
    ∀ x, y: (Start Matrix after move equals matrix before move except the new Disk)
      x >= 0 and 
      x < xMax and 
      y >= 0 and 
      y < yMax and 
      (x != x0 + pmEx or 
      y != game.matrix.yEmpty(x0 + pmEx)):
      game.afterMove(x0 + pmEx).matrix(x, y) = game.matrix(x, y)
    ∀end x, y (End Matrix after move equals matrix before move except the new Disk)
  Ǝend x0, y0 (End Horizontal Pattern with left coordinates x0, y0) or 
  Ǝ x0, y0: (Start Diagonal Up Pattern with bottom-left coordinates x0, y0)
    x0 >= 0 and 
    x0 < xMax - conn and 
    y0 >= 0 and 
    y0 < yMax - conn:
    ∀ extent: (Start All Extent: Connect in a Diagonal Up Row Pattern)
      extent >= 0 and 
      extent < conn:
      game.afterMove(x0 + pmEx).matrix(x0 + extent, y0 + extent) = player
    ∀end extent (End All Extent: Connect in a Diagonal Up Row Pattern) and 
    Ǝ pmEx: (Start Exists Previous Move Extent with Empty Position Above)
      pmEx >= 0 and 
      pmEx < conn:
      game.afterMove(x0 + pmEx).matrix.yEmpty(x0 + pmEx) = y0 + pmEx + 1
    Ǝend pmEx (End Exists Previous Move Extent with Empty Position Above) and 
    game.matrix.yEmpty(x0 + pmEx) < yMax - 1 and 
    game.afterMove(x0 + pmEx).toMove = opponent(game.toMove) and 
    game.afterMove(x0 + pmEx).matrix(x0 + pmEx, game.matrix.yEmpty(x0 + pmEx)) = game.toMove and 
    game.afterMove(x0 + pmEx).matrix.yEmpty(x0 + pmEx) = game.matrix.yEmpty(x0 + pmEx) + 1 and 
    ∀ x, y: (Start Matrix after move equals matrix before move except the new Disk)
      x >= 0 and 
      x < xMax and 
      y >= 0 and 
      y < yMax and 
      (x != x0 + pmEx or 
      y != game.matrix.yEmpty(x0 + pmEx)):
      game.afterMove(x0 + pmEx).matrix(x, y) = game.matrix(x, y)
    ∀end x, y (End Matrix after move equals matrix before move except the new Disk)
  Ǝend x0, y0 (End Diagonal Up Pattern with bottom-left coordinates x0, y0) or 
  Ǝ x0, y0: (Start Diagonal Down Pattern with top-left coordinates x0, y0)
    x0 >= 0 and 
    x0 < xMax - conn and 
    y0 >= conn and 
    y0 < yMax:
    ∀ extent: (Start All Extent: Connect in a Diagonal Down Row Pattern)
      extent >= 0 and 
      extent < conn:
      game.afterMove(x0 + pmEx).matrix(x0 + extent, y0 - extent) = player
    ∀end extent (End All Extent: Connect in a Diagonal Down Row Pattern) and 
    Ǝ pmEx: (Start Exists Previous Move Extent with Empty Position Above)
      pmEx >= 0 and 
      pmEx < conn:
      game.afterMove(x0 + pmEx).matrix.yEmpty(x0 + pmEx) = y0 - pmEx + 1
    Ǝend pmEx (End Exists Previous Move Extent with Empty Position Above) and 
    game.matrix.yEmpty(x0 + pmEx) < yMax - 1 and 
    game.afterMove(x0 + pmEx).toMove = opponent(game.toMove) and 
    game.afterMove(x0 + pmEx).matrix(x0 + pmEx, game.matrix.yEmpty(x0 + pmEx)) = game.toMove and 
    game.afterMove(x0 + pmEx).matrix.yEmpty(x0 + pmEx) = game.matrix.yEmpty(x0 + pmEx) + 1 and 
    ∀ x, y: (Start Matrix after move equals matrix before move except the new Disk)
      x >= 0 and 
      x < xMax and 
      y >= 0 and 
      y < yMax and 
      (x != x0 + pmEx or 
      y != game.matrix.yEmpty(x0 + pmEx)):
      game.afterMove(x0 + pmEx).matrix(x, y) = game.matrix(x, y)
    ∀end x, y (End Matrix after move equals matrix before move except the new Disk)
  Ǝend x0, y0 (End Diagonal Down Pattern with top-left coordinates x0, y0)) and 
  game.afterMove(xMove).toMove = opponent(player)
Ǝend xMove (End Exists Move Concept) and 
game.toMove = player and 
game.matrix.pppp(opponent(player)) = false
Step 6. From the two game.afterMove(x0).matrix.yEmpty(x0) statements the system solves game.matrix.yEmpty(x0) = y0 + conn - 1 for the vertical Ǝ x0, y0 pattern, from the two game.afterMove(x0 + pmEx).matrix.yEmpty(x0 + pmEx) statements the system solves game.matrix.yEmpty(x0 + pmEx) = y0 for the horizontal Ǝ x0, y0 pattern, game.matrix.yEmpty(x0 + pmEx) = y0 + pmEx for the diagonal up pattern and game.matrix.yEmpty(x0 + pmEx) = y0 - pmEx for the diagonal down pattern, adds these new statements and substitutes the left with the right of the above equations in the concerned Ǝ x0, y0 patterns. <=>
 
Ǝ xMove: (Start Exists Move Concept)
  xMove >= 0 and 
  xMove < xMax:
  (Ǝ x0, y0: (Start Vertical Pattern with bottom coordinates x0, y0)
    x0 >= 0 and 
    x0 < xMax and 
    y0 >= 0 and 
    y0 < yMax - conn:
    ∀ extent: (Start All Extent: Connect in a Vertical Row Pattern)
      extent >= 0 and 
      extent < conn:
      game.afterMove(x0).matrix(x0, y0 + extent) = player
    ∀end extent (End All Extent: Connect in a Vertical Row Pattern) and 
    game.afterMove(x0).matrix.yEmpty(x0) = y0 + conn and 
    y0 + conn - 1 < yMax - 1 and 
    game.afterMove(x0).toMove = opponent(game.toMove) and 
    game.afterMove(x0).matrix(x0, game.matrix.yEmpty(x0)) = game.toMove and 
    game.afterMove(x0).matrix.yEmpty(x0) = y0 + conn - 1 + 1 and 
    ∀ x, y: (Start Matrix after move equals matrix before move except the new Disk)
      x >= 0 and 
      x < xMax and 
      y >= 0 and 
      y < yMax and 
      (x != x0 or 
      y != y0 + conn - 1):
      game.afterMove(x0).matrix(x, y) = game.matrix(x, y)
    ∀end x, y (End Matrix after move equals matrix before move except the new Disk) and 
    game.matrix.yEmpty(x0) = y0 + conn - 1
  Ǝend x0, y0 (End Vertical Pattern with bottom coordinates x0, y0) or 
  Ǝ x0, y0: (Start Horizontal Pattern with left coordinates x0, y0)
    x0 >= 0 and 
    x0 < xMax - conn and 
    y0 >= 0 and 
    y0 < yMax:
    ∀ extent: (Start All Extent: Connect in a Horizontal Row Pattern)
      extent >= 0 and 
      extent < conn:
      game.afterMove(x0 + pmEx).matrix(x0 + extent, y0) = player
    ∀end extent (End All Extent: Connect in a Horizontal Row Pattern) and 
    Ǝ pmEx: (Start Exists Previous Move Extent with Empty Position Above)
      pmEx >= 0 and 
      pmEx < conn:
      game.afterMove(x0 + pmEx).matrix.yEmpty(x0 + pmEx) = y0 + 1 and 
      game.matrix.yEmpty(x0 + pmEx) = y0
    Ǝend pmEx (End Exists Previous Move Extent with Empty Position Above) and 
    y0 < yMax - 1 and 
    game.afterMove(x0 + pmEx).toMove = opponent(game.toMove) and 
    game.afterMove(x0 + pmEx).matrix(x0 + pmEx, y0) = game.toMove and 
    game.afterMove(x0 + pmEx).matrix.yEmpty(x0 + pmEx) = y0 + 1 and 
    ∀ x, y: (Start Matrix after move equals matrix before move except the new Disk)
      x >= 0 and 
      x < xMax and 
      y >= 0 and 
      y < yMax and 
      (x != x0 + pmEx or 
      y != y0):
      game.afterMove(x0 + pmEx).matrix(x, y) = game.matrix(x, y)
    ∀end x, y (End Matrix after move equals matrix before move except the new Disk)
  Ǝend x0, y0 (End Horizontal Pattern with left coordinates x0, y0) or 
  Ǝ x0, y0: (Start Diagonal Up Pattern with bottom-left coordinates x0, y0)
    x0 >= 0 and 
    x0 < xMax - conn and 
    y0 >= 0 and 
    y0 < yMax - conn:
    ∀ extent: (Start All Extent: Connect in a Diagonal Up Row Pattern)
      extent >= 0 and 
      extent < conn:
      game.afterMove(x0 + pmEx).matrix(x0 + extent, y0 + extent) = player
    ∀end extent (End All Extent: Connect in a Diagonal Up Row Pattern) and 
    Ǝ pmEx: (Start Exists Previous Move Extent with Empty Position Above)
      pmEx >= 0 and 
      pmEx < conn:
      game.afterMove(x0 + pmEx).matrix.yEmpty(x0 + pmEx) = y0 + pmEx + 1 and 
      game.matrix.yEmpty(x0 + pmEx) = y0 + pmEx
    Ǝend pmEx (End Exists Previous Move Extent with Empty Position Above) and 
    y0 + pmEx < yMax - 1 and 
    game.afterMove(x0 + pmEx).toMove = opponent(game.toMove) and 
    game.afterMove(x0 + pmEx).matrix(x0 + pmEx, game.matrix.yEmpty(x0 + pmEx)) = game.toMove and 
    game.afterMove(x0 + pmEx).matrix.yEmpty(x0 + pmEx) = y0 + pmEx + 1 and 
    ∀ x, y: (Start Matrix after move equals matrix before move except the new Disk)
      x >= 0 and 
      x < xMax and 
      y >= 0 and 
      y < yMax and 
      (x != x0 + pmEx or 
      y != y0 + pmEx):
      game.afterMove(x0 + pmEx).matrix(x, y) = game.matrix(x, y)
    ∀end x, y (End Matrix after move equals matrix before move except the new Disk)
  Ǝend x0, y0 (End Diagonal Up Pattern with bottom-left coordinates x0, y0) or 
  Ǝ x0, y0: (Start Diagonal Down Pattern with top-left coordinates x0, y0)
    x0 >= 0 and 
    x0 < xMax - conn and 
    y0 >= conn and 
    y0 < yMax:
    ∀ extent: (Start All Extent: Connect in a Diagonal Down Row Pattern)
      extent >= 0 and 
      extent < conn:
      game.afterMove(x0 + pmEx).matrix(x0 + extent, y0 - extent) = player
    ∀end extent (End All Extent: Connect in a Diagonal Down Row Pattern) and 
    Ǝ pmEx: (Start Exists Previous Move Extent with Empty Position Above)
      pmEx >= 0 and 
      pmEx < conn:
      game.afterMove(x0 + pmEx).matrix.yEmpty(x0 + pmEx) = y0 - pmEx + 1 and 
      game.matrix.yEmpty(x0 + pmEx) = y0 - pmEx
    Ǝend pmEx (End Exists Previous Move Extent with Empty Position Above) and 
    y0 - pmEx < yMax - 1 and 
    game.afterMove(x0 + pmEx).toMove = opponent(game.toMove) and 
    game.afterMove(x0 + pmEx).matrix(x0 + pmEx, game.matrix.yEmpty(x0 + pmEx)) = game.toMove and 
    game.afterMove(x0 + pmEx).matrix.yEmpty(x0 + pmEx) = y0 - pmEx + 1 and 
    ∀ x, y: (Start Matrix after move equals matrix before move except the new Disk)
      x >= 0 and 
      x < xMax and 
      y >= 0 and 
      y < yMax and 
      (x != x0 + pmEx or 
      y != y0 - pmEx):
      game.afterMove(x0 + pmEx).matrix(x, y) = game.matrix(x, y)
    ∀end x, y (End Matrix after move equals matrix before move except the new Disk)
  Ǝend x0, y0 (End Diagonal Down Pattern with top-left coordinates x0, y0)) and 
  game.afterMove(xMove).toMove = opponent(player)
Ǝend xMove (End Exists Move Concept) and 
game.toMove = player and 
game.matrix.pppp(opponent(player)) = false
Step 7. The system applies in the vertical Ǝ x0, y0 pattern ∀ x, y onto ∀ extent to substitute game.afterMove(x0).matrix(x0, y0 + extent) in the rule of the ∀ extent with game.matrix(x0, y0 + extent) (this is the game board before the 1 winning move). As such the system also adds the (x != x0 or y != y0 + conn - 1) delimiter rule from ∀ x, y into the ∀ extent. The above substitution (equality rule) also implies the substitution of x with x0 and of y with y0 + extent in the latter added delimiter rule. The system does similar (with variation in the substitutions to be applied) for the horizontal, diagonal up and down Ǝ x0, y0 patterns. <=>
 
Ǝ xMove: (Start Exists Move Concept)
  xMove >= 0 and 
  xMove < xMax:
  (Ǝ x0, y0: (Start Vertical Pattern with bottom coordinates x0, y0)
    x0 >= 0 and 
    x0 < xMax and 
    y0 >= 0 and 
    y0 < yMax - conn:
    ∀ extent: (Start All Extent: Connect in a Vertical Row Pattern)
      extent >= 0 and 
      extent < conn and 
      (x0 != x0 or 
      y0 + extent != y0 + conn - 1):
      game.matrix(x0, y0 + extent) = player
    ∀end extent (End All Extent: Connect in a Vertical Row Pattern) and 
    game.afterMove(x0).matrix.yEmpty(x0) = y0 + conn and 
    y0 + conn - 1 < yMax - 1 and 
    game.afterMove(x0).toMove = opponent(game.toMove) and 
    game.afterMove(x0).matrix(x0, game.matrix.yEmpty(x0)) = game.toMove and 
    game.afterMove(x0).matrix.yEmpty(x0) = y0 + conn - 1 + 1 and 
    ∀ x, y: (Start Matrix after move equals matrix before move except the new Disk)
      x >= 0 and 
      x < xMax and 
      y >= 0 and 
      y < yMax and 
      (x != x0 or 
      y != y0 + conn - 1):
      game.afterMove(x0).matrix(x, y) = game.matrix(x, y)
    ∀end x, y (End Matrix after move equals matrix before move except the new Disk) and 
    game.matrix.yEmpty(x0) = y0 + conn - 1
  Ǝend x0, y0 (End Vertical Pattern with bottom coordinates x0, y0) or 
  Ǝ x0, y0: (Start Horizontal Pattern with left coordinates x0, y0)
    x0 >= 0 and 
    x0 < xMax - conn and 
    y0 >= 0 and 
    y0 < yMax:
    ∀ extent: (Start All Extent: Connect in a Horizontal Row Pattern)
      extent >= 0 and 
      extent < conn and 
      (x0 + extent != x0 + pmEx or 
      y0 != y0):
      game.matrix(x0 + extent, y0) = player
    ∀end extent (End All Extent: Connect in a Horizontal Row Pattern) and 
    Ǝ pmEx: (Start Exists Previous Move Extent with Empty Position Above)
      pmEx >= 0 and 
      pmEx < conn:
      game.afterMove(x0 + pmEx).matrix.yEmpty(x0 + pmEx) = y0 + 1 and 
      game.matrix.yEmpty(x0 + pmEx) = y0
    Ǝend pmEx (End Exists Previous Move Extent with Empty Position Above) and 
    y0 < yMax - 1 and 
    game.afterMove(x0 + pmEx).toMove = opponent(game.toMove) and 
    game.afterMove(x0 + pmEx).matrix(x0 + pmEx, y0) = game.toMove and 
    game.afterMove(x0 + pmEx).matrix.yEmpty(x0 + pmEx) = y0 + 1 and 
    ∀ x, y: (Start Matrix after move equals matrix before move except the new Disk)
      x >= 0 and 
      x < xMax and 
      y >= 0 and 
      y < yMax and 
      (x != x0 + pmEx or 
      y != y0):
      game.afterMove(x0 + pmEx).matrix(x, y) = game.matrix(x, y)
    ∀end x, y (End Matrix after move equals matrix before move except the new Disk)
  Ǝend x0, y0 (End Horizontal Pattern with left coordinates x0, y0) or 
  Ǝ x0, y0: (Start Diagonal Up Pattern with bottom-left coordinates x0, y0)
    x0 >= 0 and 
    x0 < xMax - conn and 
    y0 >= 0 and 
    y0 < yMax - conn:
    ∀ extent: (Start All Extent: Connect in a Diagonal Up Row Pattern)
      extent >= 0 and 
      extent < conn and 
      (x0 + extent != x0 + pmEx or 
      y0 + extent != y0 + pmEx):
      game.matrix(x0 + extent, y0 + extent) = player
    ∀end extent (End All Extent: Connect in a Diagonal Up Row Pattern) and 
    Ǝ pmEx: (Start Exists Previous Move Extent with Empty Position Above)
      pmEx >= 0 and 
      pmEx < conn:
      game.afterMove(x0 + pmEx).matrix.yEmpty(x0 + pmEx) = y0 + pmEx + 1 and 
      game.matrix.yEmpty(x0 + pmEx) = y0 + pmEx
    Ǝend pmEx (End Exists Previous Move Extent with Empty Position Above) and 
    y0 + pmEx < yMax - 1 and 
    game.afterMove(x0 + pmEx).toMove = opponent(game.toMove) and 
    game.afterMove(x0 + pmEx).matrix(x0 + pmEx, game.matrix.yEmpty(x0 + pmEx)) = game.toMove and 
    game.afterMove(x0 + pmEx).matrix.yEmpty(x0 + pmEx) = y0 + pmEx + 1 and 
    ∀ x, y: (Start Matrix after move equals matrix before move except the new Disk)
      x >= 0 and 
      x < xMax and 
      y >= 0 and 
      y < yMax and 
      (x != x0 + pmEx or 
      y != y0 + pmEx):
      game.afterMove(x0 + pmEx).matrix(x, y) = game.matrix(x, y)
    ∀end x, y (End Matrix after move equals matrix before move except the new Disk)
  Ǝend x0, y0 (End Diagonal Up Pattern with bottom-left coordinates x0, y0) or 
  Ǝ x0, y0: (Start Diagonal Down Pattern with top-left coordinates x0, y0)
    x0 >= 0 and 
    x0 < xMax - conn and 
    y0 >= conn and 
    y0 < yMax:
    ∀ extent: (Start All Extent: Connect in a Diagonal Down Row Pattern)
      extent >= 0 and 
      extent < conn and 
      (x0 + extent != x0 + pmEx or 
      y0 - extent != y0 - pmEx):
      game.matrix(x0 + extent, y0 - extent) = player
    ∀end extent (End All Extent: Connect in a Diagonal Down Row Pattern) and 
    Ǝ pmEx: (Start Exists Previous Move Extent with Empty Position Above)
      pmEx >= 0 and 
      pmEx < conn:
      game.afterMove(x0 + pmEx).matrix.yEmpty(x0 + pmEx) = y0 - pmEx + 1 and 
      game.matrix.yEmpty(x0 + pmEx) = y0 - pmEx
    Ǝend pmEx (End Exists Previous Move Extent with Empty Position Above) and 
    y0 - pmEx < yMax - 1 and 
    game.afterMove(x0 + pmEx).toMove = opponent(game.toMove) and 
    game.afterMove(x0 + pmEx).matrix(x0 + pmEx, game.matrix.yEmpty(x0 + pmEx)) = game.toMove and 
    game.afterMove(x0 + pmEx).matrix.yEmpty(x0 + pmEx) = y0 - pmEx + 1 and 
    ∀ x, y: (Start Matrix after move equals matrix before move except the new Disk)
      x >= 0 and 
      x < xMax and 
      y >= 0 and 
      y < yMax and 
      (x != x0 + pmEx or 
      y != y0 - pmEx):
      game.afterMove(x0 + pmEx).matrix(x, y) = game.matrix(x, y)
    ∀end x, y (End Matrix after move equals matrix before move except the new Disk)
  Ǝend x0, y0 (End Diagonal Down Pattern with top-left coordinates x0, y0)) and 
  game.afterMove(xMove).toMove = opponent(player)
Ǝend xMove (End Exists Move Concept) and 
game.toMove = player and 
game.matrix.pppp(opponent(player)) = false
Step 8. The system normalizes the delimiters of the ∀ extent sections. This is the system evaluates and merges these delimiters rules to a minimal set of equivalent delimiter rules. <=>
 
Ǝ xMove: (Start Exists Move Concept)
  xMove >= 0 and 
  xMove < xMax:
  (Ǝ x0, y0: (Start Vertical Pattern with bottom coordinates x0, y0)
    x0 >= 0 and 
    x0 < xMax and 
    y0 >= 0 and 
    y0 < yMax - conn:
    ∀ extent: (Start All Extent: Connect in a Vertical Row Pattern)
      extent >= 0 and 
      extent < conn - 1:
      game.matrix(x0, y0 + extent) = player
    ∀end extent (End All Extent: Connect in a Vertical Row Pattern) and 
    game.afterMove(x0).matrix.yEmpty(x0) = y0 + conn and 
    y0 + conn - 1 < yMax - 1 and 
    game.afterMove(x0).toMove = opponent(game.toMove) and 
    game.afterMove(x0).matrix(x0, game.matrix.yEmpty(x0)) = game.toMove and 
    game.afterMove(x0).matrix.yEmpty(x0) = y0 + conn - 1 + 1 and 
    ∀ x, y: (Start Matrix after move equals matrix before move except the new Disk)
      x >= 0 and 
      x < xMax and 
      y >= 0 and 
      y < yMax and 
      (x != x0 or 
      y != y0 + conn - 1):
      game.afterMove(x0).matrix(x, y) = game.matrix(x, y)
    ∀end x, y (End Matrix after move equals matrix before move except the new Disk) and 
    game.matrix.yEmpty(x0) = y0 + conn - 1
  Ǝend x0, y0 (End Vertical Pattern with bottom coordinates x0, y0) or 
  Ǝ x0, y0: (Start Horizontal Pattern with left coordinates x0, y0)
    x0 >= 0 and 
    x0 < xMax - conn and 
    y0 >= 0 and 
    y0 < yMax:
    ∀ extent: (Start All Extent: Connect in a Horizontal Row Pattern)
      extent >= 0 and 
      extent < conn and 
      extent != pmEx:
      game.matrix(x0 + extent, y0) = player
    ∀end extent (End All Extent: Connect in a Horizontal Row Pattern) and 
    Ǝ pmEx: (Start Exists Previous Move Extent with Empty Position Above)
      pmEx >= 0 and 
      pmEx < conn:
      game.afterMove(x0 + pmEx).matrix.yEmpty(x0 + pmEx) = y0 + 1 and 
      game.matrix.yEmpty(x0 + pmEx) = y0
    Ǝend pmEx (End Exists Previous Move Extent with Empty Position Above) and 
    y0 < yMax - 1 and 
    game.afterMove(x0 + pmEx).toMove = opponent(game.toMove) and 
    game.afterMove(x0 + pmEx).matrix(x0 + pmEx, y0) = game.toMove and 
    game.afterMove(x0 + pmEx).matrix.yEmpty(x0 + pmEx) = y0 + 1 and 
    ∀ x, y: (Start Matrix after move equals matrix before move except the new Disk)
      x >= 0 and 
      x < xMax and 
      y >= 0 and 
      y < yMax and 
      (x != x0 + pmEx or 
      y != y0):
      game.afterMove(x0 + pmEx).matrix(x, y) = game.matrix(x, y)
    ∀end x, y (End Matrix after move equals matrix before move except the new Disk)
  Ǝend x0, y0 (End Horizontal Pattern with left coordinates x0, y0) or 
  Ǝ x0, y0: (Start Diagonal Up Pattern with bottom-left coordinates x0, y0)
    x0 >= 0 and 
    x0 < xMax - conn and 
    y0 >= 0 and 
    y0 < yMax - conn:
    ∀ extent: (Start All Extent: Connect in a Diagonal Up Row Pattern)
      extent >= 0 and 
      extent < conn and 
      extent != pmEx:
      game.matrix(x0 + extent, y0 + extent) = player
    ∀end extent (End All Extent: Connect in a Diagonal Up Row Pattern) and 
    Ǝ pmEx: (Start Exists Previous Move Extent with Empty Position Above)
      pmEx >= 0 and 
      pmEx < conn:
      game.afterMove(x0 + pmEx).matrix.yEmpty(x0 + pmEx) = y0 + pmEx + 1 and 
      game.matrix.yEmpty(x0 + pmEx) = y0 + pmEx
    Ǝend pmEx (End Exists Previous Move Extent with Empty Position Above) and 
    y0 + pmEx < yMax - 1 and 
    game.afterMove(x0 + pmEx).toMove = opponent(game.toMove) and 
    game.afterMove(x0 + pmEx).matrix(x0 + pmEx, game.matrix.yEmpty(x0 + pmEx)) = game.toMove and 
    game.afterMove(x0 + pmEx).matrix.yEmpty(x0 + pmEx) = y0 + pmEx + 1 and 
    ∀ x, y: (Start Matrix after move equals matrix before move except the new Disk)
      x >= 0 and 
      x < xMax and 
      y >= 0 and 
      y < yMax and 
      (x != x0 + pmEx or 
      y != y0 + pmEx):
      game.afterMove(x0 + pmEx).matrix(x, y) = game.matrix(x, y)
    ∀end x, y (End Matrix after move equals matrix before move except the new Disk)
  Ǝend x0, y0 (End Diagonal Up Pattern with bottom-left coordinates x0, y0) or 
  Ǝ x0, y0: (Start Diagonal Down Pattern with top-left coordinates x0, y0)
    x0 >= 0 and 
    x0 < xMax - conn and 
    y0 >= conn and 
    y0 < yMax:
    ∀ extent: (Start All Extent: Connect in a Diagonal Down Row Pattern)
      extent >= 0 and 
      extent < conn and 
      extent != pmEx:
      game.matrix(x0 + extent, y0 - extent) = player
    ∀end extent (End All Extent: Connect in a Diagonal Down Row Pattern) and 
    Ǝ pmEx: (Start Exists Previous Move Extent with Empty Position Above)
      pmEx >= 0 and 
      pmEx < conn:
      game.afterMove(x0 + pmEx).matrix.yEmpty(x0 + pmEx) = y0 - pmEx + 1 and 
      game.matrix.yEmpty(x0 + pmEx) = y0 - pmEx
    Ǝend pmEx (End Exists Previous Move Extent with Empty Position Above) and 
    y0 - pmEx < yMax - 1 and 
    game.afterMove(x0 + pmEx).toMove = opponent(game.toMove) and 
    game.afterMove(x0 + pmEx).matrix(x0 + pmEx, game.matrix.yEmpty(x0 + pmEx)) = game.toMove and 
    game.afterMove(x0 + pmEx).matrix.yEmpty(x0 + pmEx) = y0 - pmEx + 1 and 
    ∀ x, y: (Start Matrix after move equals matrix before move except the new Disk)
      x >= 0 and 
      x < xMax and 
      y >= 0 and 
      y < yMax and 
      (x != x0 + pmEx or 
      y != y0 - pmEx):
      game.afterMove(x0 + pmEx).matrix(x, y) = game.matrix(x, y)
    ∀end x, y (End Matrix after move equals matrix before move except the new Disk)
  Ǝend x0, y0 (End Diagonal Down Pattern with top-left coordinates x0, y0)) and 
  game.afterMove(xMove).toMove = opponent(player)
Ǝend xMove (End Exists Move Concept) and 
game.toMove = player and 
game.matrix.pppp(opponent(player)) = false
Step 9. The system matches the green rules and quantifiers in the above step with the equivalence definition of the matrix.reppp(player, 0, rex) pattern (see predefined patterns below) and deducts (proofs) as such the re0ppp pattern. In other words step 9 recognizes the re0ppp pattern in the result of the deduction upto step 8. The rules and quantifiers are matched for the vertical, horizontal and diagonal up and down Ǝ x0, y0 patterns. <=>
 
game.matrix.reppp(player, 0, rex) = true and 
game.toMove = player and 
game.matrix.pppp(opponent(player)) = false

Connect Four Classes, Rules, Quantifiers and Predefined and Deduced Pattern Functions 
xMax = 7
yMax = 6
conn = 4
opponent(1) = 2
opponent(2) = 1

game.connects4InMoves(player, 1) <=> (Predefined Pattern Function)
Ǝ xMove: (Start Exists Move Concept)
  xMove >= 0 and 
  xMove < xMax:
  game.afterMove(xMove).connects4InMoves(player, 0) = true
Ǝend xMove (End Exists Move Concept) and 
game.toMove = player and 
game.matrix.pppp(opponent(player)) = false

game.connects4InMoves(player, 2) <=> (Predefined Pattern Function)
∀ xMove: (Start For All Move Concept)
  xMove >= 0 and 
  xMove < xMax and 
  game.matrix.yEmpty(xMove) < yMax - 1:
  game.afterMove(xMove).connects4InMoves(player, 1) = true
∀end xMove (End For All Move Concept)

game.connects4InMoves(player, 3) <=> (Predefined Pattern Function)
Ǝ xExistsMove: (Start Exists Move Concept)
  xExistsMove >= 0 and 
  xExistsMove < xMax:
  game.afterMove(xExistsMove).connects4InMoves(player, 2) = true
Ǝend xExistsMove (End Exists Move Concept) and 
game.connects4InMoves(player, 1) = false

game.connects4InMoves(player, 4) <=> (Predefined Pattern Function)
∀ xAll4Move: (Start For All Move Concept)
  xAll4Move >= 0 and 
  xAll4Move < xMax and 
  game.matrix.yEmpty(xAll4Move) < yMax - 1:
  game.afterMove(xAll4Move).connects4InMoves(player, 3) = true
∀end xAll4Move (End For All Move Concept)

matrix.pppp(player) <=> (Predefined Pattern Function)
Ǝ x0, y0: (Start Vertical Pattern with bottom coordinates x0, y0)
  x0 >= 0 and 
  x0 < xMax and 
  y0 >= 0 and 
  y0 < yMax - conn:
  ∀ extent: (Start All Extent: Connect in a Vertical Row Pattern)
    extent >= 0 and 
    extent < conn:
    matrix(x0, y0 + extent) = player
  ∀end extent (End All Extent: Connect in a Vertical Row Pattern) and 
  matrix.yEmpty(x0) = y0 + conn
Ǝend x0, y0 (End Vertical Pattern with bottom coordinates x0, y0) or 
Ǝ x0, y0: (Start Horizontal Pattern with left coordinates x0, y0)
  x0 >= 0 and 
  x0 < xMax - conn and 
  y0 >= 0 and 
  y0 < yMax:
  ∀ extent: (Start All Extent: Connect in a Horizontal Row Pattern)
    extent >= 0 and 
    extent < conn:
    matrix(x0 + extent, y0) = player
  ∀end extent (End All Extent: Connect in a Horizontal Row Pattern) and 
  Ǝ pmEx: (Start Exists Previous Move Extent with Empty Position Above)
    pmEx >= 0 and 
    pmEx < conn:
    matrix.yEmpty(x0 + pmEx) = y0 + 1
  Ǝend pmEx (End Exists Previous Move Extent with Empty Position Above)
Ǝend x0, y0 (End Horizontal Pattern with left coordinates x0, y0) or 
Ǝ x0, y0: (Start Diagonal Up Pattern with bottom-left coordinates x0, y0)
  x0 >= 0 and 
  x0 < xMax - conn and 
  y0 >= 0 and 
  y0 < yMax - conn:
  ∀ extent: (Start All Extent: Connect in a Diagonal Up Row Pattern)
    extent >= 0 and 
    extent < conn:
    matrix(x0 + extent, y0 + extent) = player
  ∀end extent (End All Extent: Connect in a Diagonal Up Row Pattern) and 
  Ǝ pmEx: (Start Exists Previous Move Extent with Empty Position Above)
    pmEx >= 0 and 
    pmEx < conn:
    matrix.yEmpty(x0 + pmEx) = y0 + pmEx + 1
  Ǝend pmEx (End Exists Previous Move Extent with Empty Position Above)
Ǝend x0, y0 (End Diagonal Up Pattern with bottom-left coordinates x0, y0) or 
Ǝ x0, y0: (Start Diagonal Down Pattern with top-left coordinates x0, y0)
  x0 >= 0 and 
  x0 < xMax - conn and 
  y0 >= conn and 
  y0 < yMax:
  ∀ extent: (Start All Extent: Connect in a Diagonal Down Row Pattern)
    extent >= 0 and 
    extent < conn:
    matrix(x0 + extent, y0 - extent) = player
  ∀end extent (End All Extent: Connect in a Diagonal Down Row Pattern) and 
  Ǝ pmEx: (Start Exists Previous Move Extent with Empty Position Above)
    pmEx >= 0 and 
    pmEx < conn:
    matrix.yEmpty(x0 + pmEx) = y0 - pmEx + 1
  Ǝend pmEx (End Exists Previous Move Extent with Empty Position Above)
Ǝend x0, y0 (End Diagonal Down Pattern with top-left coordinates x0, y0)

game.connects4InMoves(player, 0) <=> (Predefined Pattern Function)
game.matrix.pppp(player) = true and 
game.toMove = opponent(player)

game.afterMove(xMove) <=> (Predefined Pattern Function)
game.matrix.yEmpty(xMove) < yMax - 1 and 
game.afterMove(xMove).toMove = opponent(game.toMove) and 
game.afterMove(xMove).matrix(xMove, game.matrix.yEmpty(xMove)) = game.toMove and 
game.afterMove(xMove).matrix.yEmpty(xMove) = game.matrix.yEmpty(xMove) + 1 and 
∀ x, y: (Start Matrix after move equals matrix before move except the new Disk)
  x >= 0 and 
  x < xMax and 
  y >= 0 and 
  y < yMax and 
  (x != xMove or 
  y != game.matrix.yEmpty(xMove)):
  game.afterMove(xMove).matrix(x, y) = game.matrix(x, y)
∀end x, y (End Matrix after move equals matrix before move except the new Disk)

matrix.reppp(player, red, rex) <=> (Predefined Pattern Function)
Ǝ x0, y0: (Start Vertical Pattern with bottom coordinates x0, y0)
  x0 >= 0 and 
  x0 < xMax and 
  y0 >= 0 and 
  y0 < yMax - conn:
  ∀ extent: (Start All Extent: Connect in a Vertical Row Pattern)
    extent >= 0 and 
    extent < conn - 1:
    matrix(x0, y0 + extent) = player
  ∀end extent (End All Extent: Connect in a Vertical Row Pattern) and 
  matrix.yEmpty(rex) = y0 + conn - 1 - red and 
  rex = x0
Ǝend x0, y0 (End Vertical Pattern with bottom coordinates x0, y0) or 
Ǝ x0, y0: (Start Horizontal Pattern with left coordinates x0, y0)
  x0 >= 0 and 
  x0 < xMax - conn and 
  y0 >= 0 and 
  y0 < yMax:
  ∀ extent: (Start All Extent: Connect in a Horizontal Row Pattern)
    extent >= 0 and 
    extent < conn and 
    extent != rexEx:
    matrix(x0 + extent, y0) = player
  ∀end extent (End All Extent: Connect in a Horizontal Row Pattern) and 
  Ǝ rexEx: (Start re0 Extent: Extent of the Rotatable Empty position in the re0ppp Pattern)
    rexEx >= 0 and 
    rexEx < conn:
    matrix.yEmpty(rex) = y0 - red and 
    rex = x0 + rexEx
  Ǝend rexEx (End re0 Extent: Extent of the Rotatable Empty position in the re0ppp Pattern)
Ǝend x0, y0 (End Horizontal Pattern with left coordinates x0, y0) or 
Ǝ x0, y0: (Start Diagonal Up Pattern with bottom-left coordinates x0, y0)
  x0 >= 0 and 
  x0 < xMax - conn and 
  y0 >= 0 and 
  y0 < yMax - conn:
  ∀ extent: (Start All Extent: Connect in a Diagonal Up Row Pattern)
    extent >= 0 and 
    extent < conn and 
    extent != rexEx:
    matrix(x0 + extent, y0 + extent) = player
  ∀end extent (End All Extent: Connect in a Diagonal Up Row Pattern) and 
  Ǝ rexEx: (Start re0 Extent: Extent of the Rotatable Empty position in the re0ppp Pattern)
    rexEx >= 0 and 
    rexEx < conn:
    matrix.yEmpty(rex) = y0 + rexEx - red and 
    rex = x0 + rexEx
  Ǝend rexEx (End re0 Extent: Extent of the Rotatable Empty position in the re0ppp Pattern)
Ǝend x0, y0 (End Diagonal Up Pattern with bottom-left coordinates x0, y0) or 
Ǝ x0, y0: (Start Diagonal Down Pattern with top-left coordinates x0, y0)
  x0 >= 0 and 
  x0 < xMax - conn and 
  y0 >= conn and 
  y0 < yMax:
  ∀ extent: (Start All Extent: Connect in a Diagonal Down Row Pattern)
    extent >= 0 and 
    extent < conn and 
    extent != rexEx:
    matrix(x0 + extent, y0 - extent) = player
  ∀end extent (End All Extent: Connect in a Diagonal Down Row Pattern) and 
  Ǝ rexEx: (Start re0 Extent: Extent of the Rotatable Empty position in the re0ppp Pattern)
    rexEx >= 0 and 
    rexEx < conn:
    matrix.yEmpty(rex) = y0 - rexEx - red and 
    rex = x0 + rexEx
  Ǝend rexEx (End re0 Extent: Extent of the Rotatable Empty position in the re0ppp Pattern)
Ǝend x0, y0 (End Diagonal Down Pattern with top-left coordinates x0, y0)

game.connects4InMoves(player, 1) = true <=> (Deduced Pattern)
game.matrix.reppp(player, 0, rex) = true and 
game.toMove = player and 
game.matrix.pppp(opponent(player)) = false

game.afterMove(xMove).matrix.pppp(player) = true <=> (Deduced Pattern)
((game.matrix.reppp(player, 0, xMove) = true and 
game.toMove = player) or 
game.matrix.pppp(player) = true)
Informational Add: Estimated Extra Deaths 31 Million and Estimated Adverse Effects 1.9 Billion for 3 Years of Covid Killing Protocols, Sars-Cov-2 Virus and Vaccine Bioweapons. By country. Audio-video version.

Informational Add: Timelapse of almost 8 hours of relentless persistent trailing, chemtrailing, wavering and hazing trails. I'm hoping somebody can send me the detailed science about trails, about how long types of trails can last under which conditions? #2024-02-01 8:30 AM - #Beautiful #Skies+#Clouds+#Trails of #Sint-#Lievens-#Houtem - #Belgium East-#Flanders #FHD #Speed x 256: 7:45:04->1:49 - #BeautifulSkies

Informational Add: Skateboarding Hardflip

Informational Add: Vlaams LekkerBos 2023: 160m2 wild voedselbos en voedseltuin - tussenstand 2023-11-06

Informational Add: Fake Opposition: Elitarian Puppets Pretending to Oppose the Elitarian Puppets on the other side but in fact both sides acting for the same agenda of Totalitarian Control and for their Controlling Elitarian Masters. As such they keep on fooling the people, hiding the most important truths and advance more and more the Totalitarian Control agenda of their Elitarian Masters.

Informational Add: Why deflate the parasitic system? Because the parasitic-destructiveness of oversized states and corporations always leads to decay, corruption, injustice, ..., to the destruction of its many hosts, the people, the working and creative people, the maimed and dying slaves of the elites. See examples below.

Informational Add: Pattern Deduction AI in Connect Four 2023-09-21: An AI trying to do it the Human way - Pattern re0ppp I think the concept of pattern deduction will be a central and main paradigm in AI because it does not depend on huge computing power and memory size as brute force AI does. In fact pattern deduction is an attempt to simulate a more human and as such smarter form of modelling and reasoning than brute force: an AI trying to do it the human way.

Informational Add: The Parasitic System 2024-08-07: They simply evolve their-selves to extinction. Darwin at work.

Informational Add: Lokaal ruilen is een onontbeerlijke methode om het parasitaire systeem te deflateren!

Informational Add: Flemish Tasty Forest 2023: 160 m2 wild food forest and food garden - harvest score 2023-11-06

Informational Add: The Parasitic System 2023-12-13: Lets Deflate the Parasitic System!

Informational Add: Pattern Deduction AI Connect 4 in 2 Moves: An AI trying to do it the Human way-re1ppp-re0ppp I think the concept of pattern deduction will be a central and main paradigm in AI because it does not depend on huge computing power and memory size as brute force AI does. In fact pattern deduction is an attempt to simulate a more human and as such smarter form of modelling and reasoning than brute force: an AI trying to do it the human way.

Informational Add: Tumia.org is hosted and powered by One.com. Start your website with one.com - Start building your dream online with an easy-to-use and affordable website builder.

Informational Add: More Dangerous Sars-Cov-2 variants by creating biological niches for those variants and by Vaids?

Informational Add: Pattern Deduction AI in Connect Four in 3 Moves 2024-09-24: An AI trying to do it the Human way - Patterns re0re1pp, re0re0pp, re2ppp, re1ppp, re0ppp and pppp I think the concept of pattern deduction will be a central and main paradigm in AI because it does not depend on huge computing power and memory size as brute force AI does. In fact pattern deduction is an attempt to simulate a more human and as such smarter form of modelling and reasoning than brute force: an AI trying to do it the human way.

Informational Add: Estimated Extra Deaths 31 Million and Estimated Adverse Effects 1.9 Billion for 3 Years of Covid Killing Protocols, Sars-Cov-2 Virus and Vaccine Bioweapons. By country. Audio-video version.

Informational Add: Timelapse of almost 8 hours of relentless persistent trailing, chemtrailing, wavering and hazing trails. I'm hoping somebody can send me the detailed science about trails, about how long types of trails can last under which conditions? #2024-02-01 8:30 AM - #Beautiful #Skies+#Clouds+#Trails of #Sint-#Lievens-#Houtem - #Belgium East-#Flanders #FHD #Speed x 256: 7:45:04->1:49 - #BeautifulSkies

Informational Add: Skateboarding Hardflip

Informational Add: Vlaams LekkerBos 2023: 160m2 wild voedselbos en voedseltuin - tussenstand 2023-11-06

Informational Add: Fake Opposition: Elitarian Puppets Pretending to Oppose the Elitarian Puppets on the other side but in fact both sides acting for the same agenda of Totalitarian Control and for their Controlling Elitarian Masters. As such they keep on fooling the people, hiding the most important truths and advance more and more the Totalitarian Control agenda of their Elitarian Masters.

Informational Add: Why deflate the parasitic system? Because the parasitic-destructiveness of oversized states and corporations always leads to decay, corruption, injustice, ..., to the destruction of its many hosts, the people, the working and creative people, the maimed and dying slaves of the elites. See examples below.

Informational Add: Pattern Deduction AI in Connect Four 2023-09-21: An AI trying to do it the Human way - Pattern re0ppp I think the concept of pattern deduction will be a central and main paradigm in AI because it does not depend on huge computing power and memory size as brute force AI does. In fact pattern deduction is an attempt to simulate a more human and as such smarter form of modelling and reasoning than brute force: an AI trying to do it the human way.

Informational Add: The Parasitic System 2024-08-07: They simply evolve their-selves to extinction. Darwin at work.
Design & Copyright 2010-2023: www.tumia.org - LAMP page generated in 0.009886 seconds. - Tribute to Mama, Papa, ... - 
Share
Informational Add Above
>>

Most hyperlinks for navigating on Tumia are implemented using Javascript. Nevertheless to enable crawlers to easily recognize those hyperlinks they also have been added in this section as plain html href hyperlinks. The latter hyperlinks are however not very useful and hence not recommended for navigating on Tumia.

|< <-- --> EN FR NL SW Ascot Residence Watamu of class Accommodation Brussels Airlines of class Airline Cat of class Animal The Belgian Monkey Caste of class Article Bamburi nature park of class Attraction Level 1 Internet Domains in Tumia of class Chart Earth Global Warming 2000 AD of class Climate Change Connect Four:PEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEEE of class Connect Four Connect Four Test Webpage of class Connect Four Test Australia of class Country Growing Beans of class Cultivation Hydroelectricity of class Energy 00e89d5.netsolhost.com of class Internet Domain java.lang.Object of class Java Class java Object.equals(java.lang.Object) checks an operator enum of class Java Code Example java.lang.Object.clone() of class Java Method Dentist Joblist in Belgium of class Joblist Airfare Comparison of class Knowledge The Dutch Language of class Language Articles in Dutch of class Learning Goal Pattern Deduction: Connect 4 in 1 Move of class Pattern Deduction Connect 4 Pattern Set 0.s.1 of class Pattern Set Connect 4 Ecosystem Pset Feed on Figs of class Pattern Set Ecosystem Bob Marley of class Person a Belgian Callbus of class Picture 's-Hertogenbosch of class Place Muffin of class Recipe Christianity of class Religion Advertising of class Sector Benelux of class Union of Countries Human-Caused Poisoning of Life and Earth: Poisoned Fields - Glyphosate, the underrated risk? of class Video Learning Geography: Maps of Belgium in Dutch of class Video Playlist Pattern Deduction: Connect 4 in 1 Move Pattern Deduction: Connect 4 in 2 Moves Pattern Deduction: Connect 4 in 3 Moves Pattern Deduction: Connect 4 in 4 Moves