class Sokoban.AlwaysMovable1 (s : State) extends Sokoban.AlwaysMovable s : Prop

• h : ∃ (s_1 : Sokoban.State), Sokoban.sys.Initial s_1 ∧ Sokoban.sys.Reachable s_1 s
• h₁ (s₁ : State) : sys.Reachable s s₁ → ∃ (s₂ : State), sys.Reachable s₁ s₂ ∧ s₁.boxes ≠ s₂.boxes
• h₂ : s.boxes.size = 1

class Sokoban.MovableBoxConjecture1 : Prop

• h : ∃ (s : State), AlwaysMovable1 s

def Sokoban.MovableBoxConjecture1.stateCnd₀ (n : ℕ) (s : State) : Prop

Equations

• Sokoban.MovableBoxConjecture1.stateCnd₀ n s = (Sokoban.AlwaysMovable1 s ∧ s.boxesReachable.size = n)

noncomputable def Sokoban.MovableBoxConjecture1.size₀ : ℕ

Equations

• Sokoban.MovableBoxConjecture1.size₀ = Nat.find! fun (n : ℕ) => ∃ (s : Sokoban.State), Sokoban.MovableBoxConjecture1.stateCnd₀ n s

noncomputable def Sokoban.MovableBoxConjecture1.state₀ : State

Equations

• Sokoban.MovableBoxConjecture1.state₀ = Classical.epsilon fun (s : Sokoban.State) => Sokoban.MovableBoxConjecture1.stateCnd₀ Sokoban.MovableBoxConjecture1.size₀ s

noncomputable def Sokoban.MovableBoxConjecture1.trBox₁ : PointZ

Equations

• Sokoban.MovableBoxConjecture1.trBox₁ = Sokoban.MovableBoxConjecture1.state₀.trBox

noncomputable def Sokoban.MovableBoxConjecture1.state₁ : State

Equations

• Sokoban.MovableBoxConjecture1.state₁ = Classical.epsilon fun (s : Sokoban.State) => Sokoban.sys.Reachable Sokoban.MovableBoxConjecture1.state₀ s ∧ s.boxes = Set'.singleton Sokoban.MovableBoxConjecture1.trBox₁

noncomputable def Sokoban.MovableBoxConjecture1.state₂ : State

Equations

• Sokoban.MovableBoxConjecture1.state₂ = Classical.epsilon fun (s : Sokoban.State) => Sokoban.sys.Reachable Sokoban.MovableBoxConjecture1.state₁ s ∧ s.boxes ≠ Set'.singleton Sokoban.MovableBoxConjecture1.trBox₁

noncomputable def Sokoban.State.box (s : State) : PointZ

Equations

• s.box = Classical.epsilon fun (p : PointZ) => p ∈ s.boxes

noncomputable def Sokoban.MovableBoxConjecture1.state₃ : State

Equations

• Sokoban.MovableBoxConjecture1.state₃ = Classical.epsilon fun (s : Sokoban.State) => s.box = Sokoban.MovableBoxConjecture1.trBox₁ ∧ ∃ (s' : Sokoban.State), Sokoban.sys.Reachable Sokoban.MovableBoxConjecture1.state₂ s' ∧ s'.BoxPushed s

noncomputable def Sokoban.MovableBoxConjecture1.state₃' : State

Equations

• Sokoban.MovableBoxConjecture1.state₃' = Classical.epsilon fun (s : Sokoban.State) => Sokoban.sys.Reachable Sokoban.MovableBoxConjecture1.state₂ s ∧ s.BoxPushed Sokoban.MovableBoxConjecture1.state₃