theorem Sokoban.MovableBoxConjecture1.exi_stateCnd₀ [H : MovableBoxConjecture1] : ∃ (n : ℕ) (s : State), stateCnd₀ n s

theorem Sokoban.MovableBoxConjecture1.size₀_spec' [H : MovableBoxConjecture1] : (∃ (s : State), stateCnd₀ size₀ s) ∧ ∀ (n : ℕ), (∃ (s : State), stateCnd₀ n s) → size₀ ≤ n

theorem Sokoban.MovableBoxConjecture1.size₀_spec [H : MovableBoxConjecture1] : ∃ (s : State), stateCnd₀ size₀ s

theorem Sokoban.MovableBoxConjecture1.size₀_le' [H : MovableBoxConjecture1] {n : ℕ} (h : ∃ (s : State), stateCnd₀ n s) : size₀ ≤ n

theorem Sokoban.MovableBoxConjecture1.size₀_le [H : MovableBoxConjecture1] {n : ℕ} {s : State} (h : stateCnd₀ n s) : size₀ ≤ n

@[simp]

theorem Sokoban.MovableBoxConjecture1.state₀_spec [H : MovableBoxConjecture1] : stateCnd₀ size₀ state₀

@[simp]

instance Sokoban.MovableBoxConjecture1.alwaysMovable1_state₀ [H : MovableBoxConjecture1] : AlwaysMovable1 state₀

@[simp]

theorem Sokoban.MovableBoxConjecture1.stateCnd₀_self {s : State} : stateCnd₀ s.boxesReachable.size s ↔ AlwaysMovable1 s

theorem Sokoban.MovableBoxConjecture1.state₀_size_boxesReachable_le {s : State} [H : MovableBoxConjecture1] (h : stateCnd₀ size₀ s) : s.boxesReachable.size ≤ state₀.boxesReachable.size

@[simp]

theorem Sokoban.MovableBoxConjecture1.size_boxes_of_alwaysMovable1 {s : State} [hs : AlwaysMovable1 s] : s.boxes.size = 1

@[simp]

theorem Sokoban.MovableBoxConjecture1.boxes_state₀_ne_empty [H : MovableBoxConjecture1] : state₀.boxes ≠ ∅

@[simp]

theorem Sokoban.MovableBoxConjecture1.trBox₁_mem [H : MovableBoxConjecture1] : trBox₁ ∈ state₀.boxesReachable

theorem Sokoban.MovableBoxConjecture1.trBox₁_spec [H : MovableBoxConjecture1] {p : PointZ} (h : p ∈ state₀.boxesReachable) : trBox₁.y ≤ p.y ∧ (trBox₁.y = p.y → p.x ≤ trBox₁.x)

theorem Sokoban.MovableBoxConjecture1.state₁_spec [H : MovableBoxConjecture1] : sys.Reachable state₀ state₁ ∧ state₁.boxes = Set'.singleton trBox₁

@[simp]

theorem Sokoban.MovableBoxConjecture1.reachable_state₀_state₁ [H : MovableBoxConjecture1] : sys.Reachable state₀ state₁

@[simp]

theorem Sokoban.MovableBoxConjecture1.boxes_state₁ [H : MovableBoxConjecture1] : state₁.boxes = Set'.singleton trBox₁

theorem Sokoban.MovableBoxConjecture1.alwaysMovable1_of_reachable {s s₁ : State} [hs : AlwaysMovable1 s] (h : sys.Reachable s s₁) : AlwaysMovable1 s₁

@[simp]

instance Sokoban.MovableBoxConjecture1.alwaysMovable1_state₁ [H : MovableBoxConjecture1] : AlwaysMovable1 state₁

theorem Sokoban.MovableBoxConjecture1.state₂_spec [H : MovableBoxConjecture1] : sys.Reachable state₁ state₂ ∧ state₂.boxes ≠ Set'.singleton trBox₁

@[simp]

theorem Sokoban.MovableBoxConjecture1.reachable_state₁_state₂ [H : MovableBoxConjecture1] : sys.Reachable state₁ state₂

@[simp]

theorem Sokoban.MovableBoxConjecture1.boxes_state₂_ne [H : MovableBoxConjecture1] : state₂.boxes ≠ Set'.singleton trBox₁

@[simp]

theorem Sokoban.MovableBoxConjecture1.reachable_state₀_state₂ [H : MovableBoxConjecture1] : sys.Reachable state₀ state₂

@[simp]

theorem Sokoban.MovableBoxConjecture1.points_state₁ [H : MovableBoxConjecture1] : state₁.points = state₀.points

@[simp]

theorem Sokoban.MovableBoxConjecture1.points_state₂ [H : MovableBoxConjecture1] : state₂.points = state₀.points

@[simp]

theorem Sokoban.MovableBoxConjecture1.trBox₁_mem_points_state₀ [H : MovableBoxConjecture1] : trBox₁ ∈ state₀.points

@[simp]

theorem Sokoban.MovableBoxConjecture1.boxesReachable_state₂_subset_boxesReachable_state₀ [H : MovableBoxConjecture1] : state₂.boxesReachable ⊆ state₀.boxesReachable

@[simp]

instance Sokoban.MovableBoxConjecture1.alwaysMovable1_state₂ [H : MovableBoxConjecture1] : AlwaysMovable1 state₂

@[simp]

theorem Sokoban.MovableBoxConjecture1.size_boxesReachable_state₀ [H : MovableBoxConjecture1] : state₀.boxesReachable.size = size₀

theorem Sokoban.MovableBoxConjecture1.size₀_eq [H : MovableBoxConjecture1] : size₀ = state₀.boxesReachable.size

@[simp]

theorem Sokoban.MovableBoxConjecture1.size₀_le_of_alwaysMovable1 [H : MovableBoxConjecture1] {s : State} [hs : AlwaysMovable1 s] : size₀ ≤ s.boxesReachable.size

@[simp]

theorem Sokoban.MovableBoxConjecture1.size_boxesReachable_state₁ [H : MovableBoxConjecture1] : state₁.boxesReachable.size = size₀

@[simp]

theorem Sokoban.MovableBoxConjecture1.size_boxesReachable_state₂ [H : MovableBoxConjecture1] : state₂.boxesReachable.size = size₀

@[simp]

theorem Sokoban.MovableBoxConjecture1.trBox₁_mem_boxesReachable_state₂ [H : MovableBoxConjecture1] : trBox₁ ∈ state₂.boxesReachable

@[simp]

theorem Sokoban.MovableBoxConjecture1.not_trBox₁_mem_boxes_state₀ [H : MovableBoxConjecture1] : trBox₁ ∉ state₂.boxes

theorem Sokoban.MovableBoxConjecture1.box_mem_boxes_of {s : State} (h : s.boxes.size ≠ 0) : s.box ∈ s.boxes

@[simp]

theorem Sokoban.MovableBoxConjecture1.box_mem_boxes_of_alwaysMovable1 {s : State} [hs : AlwaysMovable1 s] : s.box ∈ s.boxes

@[simp]

theorem Sokoban.MovableBoxConjecture1.singleton_box {s : State} [hs : AlwaysMovable1 s] : Set'.singleton s.box = s.boxes

theorem Sokoban.MovableBoxConjecture1.boxes_eq_singleton_box {s : State} [hs : AlwaysMovable1 s] : s.boxes = Set'.singleton s.box

@[simp]

theorem Sokoban.MovableBoxConjecture1.box_state₁ [H : MovableBoxConjecture1] : state₁.box = trBox₁

@[simp]

theorem Sokoban.MovableBoxConjecture1.box_state₂_ne_trBox₁ [H : MovableBoxConjecture1] : state₂.box ≠ trBox₁

theorem Sokoban.MovableBoxConjecture1.box_eq_of_mem_boxes {s : State} {p : PointZ} [hs : AlwaysMovable1 s] (h : p ∈ s.boxes) : s.box = p

theorem Sokoban.MovableBoxConjecture1.state₃_spec [H : MovableBoxConjecture1] : state₃.box = trBox₁ ∧ ∃ (s' : State), sys.Reachable state₂ s' ∧ s'.BoxPushed state₃

theorem Sokoban.MovableBoxConjecture1.state₃'_spec [H : MovableBoxConjecture1] : sys.Reachable state₂ state₃' ∧ state₃'.BoxPushed state₃

@[simp]

theorem Sokoban.MovableBoxConjecture1.box_state₃ [H : MovableBoxConjecture1] : state₃.box = trBox₁

@[simp]

theorem Sokoban.MovableBoxConjecture1.reachable_state₂_state₃' [H : MovableBoxConjecture1] : sys.Reachable state₂ state₃'

@[simp]

theorem Sokoban.MovableBoxConjecture1.boxPushed_state₃'_state₃ [H : MovableBoxConjecture1] : state₃'.BoxPushed state₃

@[simp]

instance Sokoban.MovableBoxConjecture1.alwaysMovable1_state₃' [H : MovableBoxConjecture1] : AlwaysMovable1 state₃'

@[simp]

theorem Sokoban.MovableBoxConjecture1.reachable_state₃'_state₃ [H : MovableBoxConjecture1] : sys.Reachable state₃' state₃

@[simp]

instance Sokoban.MovableBoxConjecture1.alwaysMovable1_state₃ [H : MovableBoxConjecture1] : AlwaysMovable1 state₃

theorem Sokoban.MovableBoxConjecture1.player'_eq_box_of_boxPushed {s s' : State} [hs : AlwaysMovable1 s] (h : s.BoxPushed s') : s'.player = s.box

theorem Sokoban.MovableBoxConjecture1.player_state₃_eq_box_state₃' [H : MovableBoxConjecture1] : state₃.player = state₃'.box