Theorem: LoopProgram.lenOne_complete (FormalSystems/Computability/Loop.lean)

State before:
⊢ ∀ (p : LoopProgram), len p = 1 → p ∈ lenOne
Tactic:
intro p h
State after:
p : LoopProgram
h : len p = 1
⊢ p ∈ lenOne

State before:
p : LoopProgram
h : len p = 1
⊢ p ∈ lenOne
Tactic:
cases p <;> simp [len] at h <;> simp [h, lenOne, Variable.eq]
State after:
case concat
p₁✝ p₂✝ : LoopProgram
h : len p₁✝ = 0 ∧ len p₂✝ = 0
⊢ False

case loop
x✝ : Variable
p✝ : LoopProgram
h : len p✝ = 0 ∧ x✝.index = 0
⊢ False

State before:
p₁✝ p : LoopProgram
h : len p₁✝ = 0 ∧ len p = 0
⊢ False
Tactic:
case concat p =>
  apply Nat.not_le_of_gt
  apply LoopProgram.len_gt_zero p
  apply Nat.le_of_eq
  exact h.right
State after:
no goals

State before:
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ False
Tactic:
case loop p =>
  apply Nat.not_le_of_gt
  apply LoopProgram.len_gt_zero p
  apply Nat.le_of_eq
  exact h.left
State after:
no goals

State before:
p₁✝ p : LoopProgram
h : len p₁✝ = 0 ∧ len p = 0
⊢ False
Tactic:
apply Nat.not_le_of_gt
State after:
case h
p₁✝ p : LoopProgram
h : len p₁✝ = 0 ∧ len p = 0
⊢ ?n > ?m

case a
p₁✝ p : LoopProgram
h : len p₁✝ = 0 ∧ len p = 0
⊢ ?n ≤ ?m

case n
p₁✝ p : LoopProgram
h : len p₁✝ = 0 ∧ len p = 0
⊢ ℕ

case m
p₁✝ p : LoopProgram
h : len p₁✝ = 0 ∧ len p = 0
⊢ ℕ

State before:
case h
p₁✝ p : LoopProgram
h : len p₁✝ = 0 ∧ len p = 0
⊢ ?n > ?m

case a
p₁✝ p : LoopProgram
h : len p₁✝ = 0 ∧ len p = 0
⊢ ?n ≤ ?m

case n
p₁✝ p : LoopProgram
h : len p₁✝ = 0 ∧ len p = 0
⊢ ℕ

case m
p₁✝ p : LoopProgram
h : len p₁✝ = 0 ∧ len p = 0
⊢ ℕ
Tactic:
apply LoopProgram.len_gt_zero p
State after:
case a
p₁✝ p : LoopProgram
h : len p₁✝ = 0 ∧ len p = 0
⊢ len p ≤ 0

State before:
case a
p₁✝ p : LoopProgram
h : len p₁✝ = 0 ∧ len p = 0
⊢ len p ≤ 0
Tactic:
apply Nat.le_of_eq
State after:
case a.p
p₁✝ p : LoopProgram
h : len p₁✝ = 0 ∧ len p = 0
⊢ len p = 0

State before:
case a.p
p₁✝ p : LoopProgram
h : len p₁✝ = 0 ∧ len p = 0
⊢ len p = 0
Tactic:
exact h.right
State after:
no goals

State before:
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ False
Tactic:
apply Nat.not_le_of_gt
State after:
case h
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ ?n > ?m

case a
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ ?n ≤ ?m

case n
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ ℕ

case m
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ ℕ

State before:
case h
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ ?n > ?m

case a
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ ?n ≤ ?m

case n
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ ℕ

case m
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ ℕ
Tactic:
apply LoopProgram.len_gt_zero p
State after:
case a
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ len p ≤ 0

State before:
case a
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ len p ≤ 0
Tactic:
apply Nat.le_of_eq
State after:
case a.p
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ len p = 0

State before:
case a.p
x✝ : Variable
p : LoopProgram
h : len p = 0 ∧ x✝.index = 0
⊢ len p = 0
Tactic:
exact h.left
State after:
no goals