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

State before:
⊢ ∀ (p : LoopProgram), toFunction p ≠ diagonal
Tactic:
intro p h
State after:
p : LoopProgram
h : toFunction p = diagonal
⊢ False

State before:
p : LoopProgram
h : toFunction p = diagonal
⊢ False
Tactic:
apply Nat.ne_of_lt
State after:
case h
p : LoopProgram
h : toFunction p = diagonal
⊢ ?a < ?b

case a
p : LoopProgram
h : toFunction p = diagonal
⊢ ?a = ?b

case a
p : LoopProgram
h : toFunction p = diagonal
⊢ ℕ

case b
p : LoopProgram
h : toFunction p = diagonal
⊢ ℕ

State before:
case h
p : LoopProgram
h : toFunction p = diagonal
⊢ ?a < ?b

case a
p : LoopProgram
h : toFunction p = diagonal
⊢ ?a = ?b

case a
p : LoopProgram
h : toFunction p = diagonal
⊢ ℕ

case b
p : LoopProgram
h : toFunction p = diagonal
⊢ ℕ
Tactic:
. show p.toFunction p.len < diagonal p.len
  unfold diagonal
  rw [Nat.lt_add_one_iff, Finset.le_fold_max]
  apply Or.inr
  exists p; constructor
  apply ofLen_complete
  rfl
State after:
case a
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) = diagonal (len p)

State before:
case a
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) = diagonal (len p)
Tactic:
. apply congrFun
  assumption
State after:
no goals

State before:
case h
p : LoopProgram
h : toFunction p = diagonal
⊢ ?a < ?b
Tactic:
show p.toFunction p.len < diagonal p.len
State after:
case h
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) < diagonal (len p)

State before:
case h
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) < diagonal (len p)
Tactic:
unfold diagonal
State after:
case h
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) < Finset.fold max 0 (fun p_1 => toFunction p_1 (len p)) (ofLen (len p)) + 1

State before:
case h
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) < Finset.fold max 0 (fun p_1 => toFunction p_1 (len p)) (ofLen (len p)) + 1
Tactic:
rw [Nat.lt_add_one_iff, Finset.le_fold_max]
State after:
case h
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) ≤ 0 ∨ ∃ x ∈ ofLen (len p), toFunction p (len p) ≤ toFunction x (len p)

State before:
case h
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) ≤ 0 ∨ ∃ x ∈ ofLen (len p), toFunction p (len p) ≤ toFunction x (len p)
Tactic:
apply Or.inr
State after:
case h.h
p : LoopProgram
h : toFunction p = diagonal
⊢ ∃ x ∈ ofLen (len p), toFunction p (len p) ≤ toFunction x (len p)

State before:
case h.h
p : LoopProgram
h : toFunction p = diagonal
⊢ ∃ x ∈ ofLen (len p), toFunction p (len p) ≤ toFunction x (len p)
Tactic:
exists p
State after:
case h.h
p : LoopProgram
h : toFunction p = diagonal
⊢ p ∈ ofLen (len p) ∧ toFunction p (len p) ≤ toFunction p (len p)

State before:
case h.h
p : LoopProgram
h : toFunction p = diagonal
⊢ p ∈ ofLen (len p) ∧ toFunction p (len p) ≤ toFunction p (len p)
Tactic:
constructor
State after:
case h.h.left
p : LoopProgram
h : toFunction p = diagonal
⊢ p ∈ ofLen (len p)

case h.h.right
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) ≤ toFunction p (len p)

State before:
case h.h.left
p : LoopProgram
h : toFunction p = diagonal
⊢ p ∈ ofLen (len p)

case h.h.right
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) ≤ toFunction p (len p)
Tactic:
apply ofLen_complete
State after:
case h.h.right
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) ≤ toFunction p (len p)

State before:
case h.h.right
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) ≤ toFunction p (len p)
Tactic:
rfl
State after:
no goals

State before:
case a
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p (len p) = diagonal (len p)
Tactic:
apply congrFun
State after:
case a.h
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p = diagonal

State before:
case a.h
p : LoopProgram
h : toFunction p = diagonal
⊢ toFunction p = diagonal
Tactic:
assumption
State after:
no goals