inductive Sokoban.MovableBoxConjecture.Alt₁.Tile : Type

• Floor : Tile
• Player : Tile
• Box : Tile
• Wall : Tile

@[instance_reducible]

instance Sokoban.MovableBoxConjecture.Alt₁.instDecidableEqTile : DecidableEq Tile

Equations

• Sokoban.MovableBoxConjecture.Alt₁.instDecidableEqTile x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Sokoban.MovableBoxConjecture.Alt₁.State : Type

• get : ℤ × ℤ → Tile
• finite : {p : ℤ × ℤ | self.get p ≠ Tile.Wall}.Finite
• player : ∃! p : ℤ × ℤ, self.get p = Tile.Player

structure Sokoban.MovableBoxConjecture.Alt₁.Step (s t : State) : Type

• p : ℤ × ℤ
• d : ℤ × ℤ
• dist : |self.d.1| + |self.d.2| = 1
• player₁ : s.get self.p = Tile.Player
• player₂ : t.get (self.p + self.d) = Tile.Player
• floor : t.get self.p = Tile.Floor
• box : if s.get (self.p + self.d) = Tile.Box then s.get (self.p + self.d * 2) = Tile.Floor ∧ t.get (self.p + self.d * 2) = Tile.Box else s.get (self.p + self.d) = Tile.Floor ∧ s.get (self.p + self.d * 2) = t.get (self.p + self.d * 2)
• congr (q : ℤ × ℤ) (k : Fin 3) : q ≠ self.p + self.d * ↑↑k → s.get self.p = t.get self.p

inductive Sokoban.MovableBoxConjecture.Alt₁.Reachable : State → State → Prop

• refl {s : State} : Reachable s s
• step {s t t' : State} : Reachable s t → ∀ (a✝ : Step t t'), Reachable s t'

def Sokoban.MovableBoxConjecture.Alt₁.Conjecture : Prop

Equations

• Sokoban.MovableBoxConjecture.Alt₁.Conjecture = ∃ (s : Sokoban.MovableBoxConjecture.Alt₁.State), ∀ (t : Sokoban.MovableBoxConjecture.Alt₁.State), Sokoban.MovableBoxConjecture.Alt₁.Reachable s t → ∃ (t' : Sokoban.MovableBoxConjecture.Alt₁.State) (p : ℤ × ℤ), Sokoban.MovableBoxConjecture.Alt₁.Reachable t t' ∧ t.get p = Sokoban.MovableBoxConjecture.Alt₁.Tile.Box ↔ t'.get p ≠ Sokoban.MovableBoxConjecture.Alt₁.Tile.Box