internlm/Lean-Github huggingface dataset:
Theorem: signature_conbot_iff_neq
Proof state before:
case mpr.intro.intro
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬ℓ ⟨τ, τ_in⟩ = ℓ' ⟨τ, τ_in⟩
⊢ evaluate M w (signature α ℓ) → ¬evaluate M w (signature α ℓ')
Tactic:
simp_all [signature, conEval]
Proof state after:
case mpr.intro.intro
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬ℓ ⟨τ, τ_in⟩ = ℓ' ⟨τ, τ_in⟩
⊢ (∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f) →
    ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x
Theorem: signature_conbot_iff_neq
Proof state before:
case mpr.intro.intro
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬ℓ ⟨τ, τ_in⟩ = ℓ' ⟨τ, τ_in⟩
⊢ (∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f) →
    ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x
Tactic:
intro ℓ_conform
Proof state after:
case mpr.intro.intro
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬ℓ ⟨τ, τ_in⟩ = ℓ' ⟨τ, τ_in⟩
ℓ_conform : ∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f
⊢ ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x
Theorem: signature_conbot_iff_neq
Proof state before:
case mpr.intro.intro
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬ℓ ⟨τ, τ_in⟩ = ℓ' ⟨τ, τ_in⟩
ℓ_conform : ∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f
⊢ ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x
Tactic:
cases em (ℓ ⟨τ,τ_in⟩)
Proof state after:
case mpr.intro.intro.inl
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬ℓ ⟨τ, τ_in⟩ = ℓ' ⟨τ, τ_in⟩
ℓ_conform : ∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f
h✝ : ℓ ⟨τ, τ_in⟩ = true
⊢ ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x

case mpr.intro.intro.inr
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬ℓ ⟨τ, τ_in⟩ = ℓ' ⟨τ, τ_in⟩
ℓ_conform : ∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f
h✝ : ¬ℓ ⟨τ, τ_in⟩ = true
⊢ ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x
Theorem: signature_conbot_iff_neq
Proof state before:
case mpr.intro.intro.inl
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬ℓ ⟨τ, τ_in⟩ = ℓ' ⟨τ, τ_in⟩
ℓ_conform : ∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f
h✝ : ℓ ⟨τ, τ_in⟩ = true
⊢ ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x
Tactic:
specialize ℓ_conform τ τ τ_in
Proof state after:
case mpr.intro.intro.inl
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬ℓ ⟨τ, τ_in⟩ = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : (if ℓ ⟨τ, ⋯⟩ = true then τ else ~τ) = τ → evaluate M w τ
⊢ ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x
Theorem: signature_conbot_iff_neq
Proof state before:
case mpr.intro.intro.inl
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬ℓ ⟨τ, τ_in⟩ = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : (if ℓ ⟨τ, ⋯⟩ = true then τ else ~τ) = τ → evaluate M w τ
⊢ ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x
Tactic:
simp_all only [ite_true, forall_true_left]
Proof state after:
case mpr.intro.intro.inl
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬true = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : evaluate M w τ
⊢ ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x
Theorem: signature_conbot_iff_neq
Proof state before:
case mpr.intro.intro.inl
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬true = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : evaluate M w τ
⊢ ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x
Tactic:
use (~τ)
Proof state after:
case h
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬true = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : evaluate M w τ
⊢ (∃ x, ∃ (x_1 : x ∈ testsOfProgram α), (if ℓ' ⟨x, ⋯⟩ = true then x else ~x) = (~τ)) ∧ ¬evaluate M w (~τ)
Theorem: signature_conbot_iff_neq
Proof state before:
case h
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬true = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : evaluate M w τ
⊢ (∃ x, ∃ (x_1 : x ∈ testsOfProgram α), (if ℓ' ⟨x, ⋯⟩ = true then x else ~x) = (~τ)) ∧ ¬evaluate M w (~τ)
Tactic:
constructor
Proof state after:
case h.left
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬true = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : evaluate M w τ
⊢ ∃ x, ∃ (x_1 : x ∈ testsOfProgram α), (if ℓ' ⟨x, ⋯⟩ = true then x else ~x) = (~τ)

case h.right
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬true = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : evaluate M w τ
⊢ ¬evaluate M w (~τ)
Theorem: signature_conbot_iff_neq
Proof state before:
case h.left
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬true = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : evaluate M w τ
⊢ ∃ x, ∃ (x_1 : x ∈ testsOfProgram α), (if ℓ' ⟨x, ⋯⟩ = true then x else ~x) = (~τ)
Tactic:
use τ, τ_in
Proof state after:
case h
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬true = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : evaluate M w τ
⊢ (if ℓ' ⟨τ, ⋯⟩ = true then τ else ~τ) = (~τ)
Theorem: signature_conbot_iff_neq
Proof state before:
case h
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬true = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : evaluate M w τ
⊢ (if ℓ' ⟨τ, ⋯⟩ = true then τ else ~τ) = (~τ)
Tactic:
simp_all
Proof state after:
no goals
Theorem: signature_conbot_iff_neq
Proof state before:
case h.right
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬true = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : evaluate M w τ
⊢ ¬evaluate M w (~τ)
Tactic:
simp
Proof state after:
case h.right
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬true = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : evaluate M w τ
⊢ evaluate M w τ
Theorem: signature_conbot_iff_neq
Proof state before:
case h.right
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬true = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : evaluate M w τ
⊢ evaluate M w τ
Tactic:
assumption
Proof state after:
no goals
Theorem: signature_conbot_iff_neq
Proof state before:
case mpr.intro.intro.inr
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬ℓ ⟨τ, τ_in⟩ = ℓ' ⟨τ, τ_in⟩
ℓ_conform : ∀ (f x : Formula) (x_1 : x ∈ testsOfProgram α), (if ℓ ⟨x, ⋯⟩ = true then x else ~x) = f → evaluate M w f
h✝ : ¬ℓ ⟨τ, τ_in⟩ = true
⊢ ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x
Tactic:
specialize ℓ_conform (~τ) τ τ_in
Proof state after:
case mpr.intro.intro.inr
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬ℓ ⟨τ, τ_in⟩ = ℓ' ⟨τ, τ_in⟩
h✝ : ¬ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : (if ℓ ⟨τ, ⋯⟩ = true then τ else ~τ) = (~τ) → evaluate M w (~τ)
⊢ ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x
Theorem: signature_conbot_iff_neq
Proof state before:
case mpr.intro.intro.inr
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬ℓ ⟨τ, τ_in⟩ = ℓ' ⟨τ, τ_in⟩
h✝ : ¬ℓ ⟨τ, τ_in⟩ = true
ℓ_conform : (if ℓ ⟨τ, ⋯⟩ = true then τ else ~τ) = (~τ) → evaluate M w (~τ)
⊢ ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x
Tactic:
simp_all only [Bool.not_eq_true, ite_false, evaluate, forall_true_left]
Proof state after:
case mpr.intro.intro.inr
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬false = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = false
ℓ_conform : ¬evaluate M w τ
⊢ ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x
Theorem: signature_conbot_iff_neq
Proof state before:
case mpr.intro.intro.inr
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬false = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = false
ℓ_conform : ¬evaluate M w τ
⊢ ∃ x, (∃ x_1, ∃ (x_2 : x_1 ∈ testsOfProgram α), (if ℓ' ⟨x_1, ⋯⟩ = true then x_1 else ~x_1) = x) ∧ ¬evaluate M w x
Tactic:
use τ
Proof state after:
case h
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬false = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = false
ℓ_conform : ¬evaluate M w τ
⊢ (∃ x, ∃ (x_1 : x ∈ testsOfProgram α), (if ℓ' ⟨x, ⋯⟩ = true then x else ~x) = τ) ∧ ¬evaluate M w τ
Theorem: signature_conbot_iff_neq
Proof state before:
case h
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬false = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = false
ℓ_conform : ¬evaluate M w τ
⊢ (∃ x, ∃ (x_1 : x ∈ testsOfProgram α), (if ℓ' ⟨x, ⋯⟩ = true then x else ~x) = τ) ∧ ¬evaluate M w τ
Tactic:
constructor
Proof state after:
case h.left
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬false = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = false
ℓ_conform : ¬evaluate M w τ
⊢ ∃ x, ∃ (x_1 : x ∈ testsOfProgram α), (if ℓ' ⟨x, ⋯⟩ = true then x else ~x) = τ

case h.right
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬false = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = false
ℓ_conform : ¬evaluate M w τ
⊢ ¬evaluate M w τ
Theorem: signature_conbot_iff_neq
Proof state before:
case h.left
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬false = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = false
ℓ_conform : ¬evaluate M w τ
⊢ ∃ x, ∃ (x_1 : x ∈ testsOfProgram α), (if ℓ' ⟨x, ⋯⟩ = true then x else ~x) = τ
Tactic:
use τ, τ_in
Proof state after:
case h
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬false = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = false
ℓ_conform : ¬evaluate M w τ
⊢ (if ℓ' ⟨τ, ⋯⟩ = true then τ else ~τ) = τ
Theorem: signature_conbot_iff_neq
Proof state before:
case h
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬false = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = false
ℓ_conform : ¬evaluate M w τ
⊢ (if ℓ' ⟨τ, ⋯⟩ = true then τ else ~τ) = τ
Tactic:
simp_all
Proof state after:
no goals
Theorem: signature_conbot_iff_neq
Proof state before:
case h.right
α : Program
ℓ ℓ' : TP α
W : Type
M : KripkeModel W
w : W
τ : Formula
τ_in : τ ∈ testsOfProgram α
disagree : ¬false = ℓ' ⟨τ, τ_in⟩
h✝ : ℓ ⟨τ, τ_in⟩ = false
ℓ_conform : ¬evaluate M w τ
⊢ ¬evaluate M w τ
Tactic:
assumption
Proof state after:
no goals
Theorem: equiv_iff_TPequiv
Proof state before:
φ ψ : Formula
α : Program
⊢ φ≡ψ ↔ ∀ (ℓ : TP α), φ⋀signature α ℓ≡ψ⋀signature α ℓ
Tactic:
sorry
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
γ : Program
δ : List Program
α : Program
ℓ : TP α
⊢ γ ∈ δ →
    δ ∈ P α ℓ →
      if isAtomic α = true then γ = α
      else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
Tactic:
intro γ_in δ_in
Proof state after:
γ : Program
δ : List Program
α : Program
ℓ : TP α
γ_in : γ ∈ δ
δ_in : δ ∈ P α ℓ
⊢ if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
Theorem: P_goes_down
Proof state before:
γ : Program
δ : List Program
α : Program
ℓ : TP α
γ_in : γ ∈ δ
δ_in : δ ∈ P α ℓ
⊢ if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
Tactic:
cases α
Proof state after:
case atom_prog
γ : Program
δ : List Program
γ_in : γ ∈ δ
a✝ : ℕ
ℓ : TP (·a✝)
δ_in : δ ∈ P (·a✝) ℓ
⊢ if isAtomic (·a✝) = true then γ = ·a✝
  else
    if isStar (·a✝) = true then lengthOfProgram γ ≤ lengthOfProgram (·a✝) else lengthOfProgram γ < lengthOfProgram (·a✝)

case sequence
γ : Program
δ : List Program
γ_in : γ ∈ δ
a✝¹ a✝ : Program
ℓ : TP (a✝¹;'a✝)
δ_in : δ ∈ P (a✝¹;'a✝) ℓ
⊢ if isAtomic (a✝¹;'a✝) = true then γ = (a✝¹;'a✝)
  else
    if isStar (a✝¹;'a✝) = true then lengthOfProgram γ ≤ lengthOfProgram (a✝¹;'a✝)
    else lengthOfProgram γ < lengthOfProgram (a✝¹;'a✝)

case union
γ : Program
δ : List Program
γ_in : γ ∈ δ
a✝¹ a✝ : Program
ℓ : TP (a✝¹⋓a✝)
δ_in : δ ∈ P (a✝¹⋓a✝) ℓ
⊢ if isAtomic (a✝¹⋓a✝) = true then γ = (a✝¹⋓a✝)
  else
    if isStar (a✝¹⋓a✝) = true then lengthOfProgram γ ≤ lengthOfProgram (a✝¹⋓a✝)
    else lengthOfProgram γ < lengthOfProgram (a✝¹⋓a✝)

case star
γ : Program
δ : List Program
γ_in : γ ∈ δ
a✝ : Program
ℓ : TP (∗a✝)
δ_in : δ ∈ P (∗a✝) ℓ
⊢ if isAtomic (∗a✝) = true then γ = (∗a✝)
  else
    if isStar (∗a✝) = true then lengthOfProgram γ ≤ lengthOfProgram (∗a✝) else lengthOfProgram γ < lengthOfProgram (∗a✝)

case test
γ : Program
δ : List Program
γ_in : γ ∈ δ
a✝ : Formula
ℓ : TP (?'a✝)
δ_in : δ ∈ P (?'a✝) ℓ
⊢ if isAtomic (?'a✝) = true then γ = (?'a✝)
  else
    if isStar (?'a✝) = true then lengthOfProgram γ ≤ lengthOfProgram (?'a✝)
    else lengthOfProgram γ < lengthOfProgram (?'a✝)
Theorem: P_goes_down
Proof state before:
case atom_prog
γ : Program
δ : List Program
γ_in : γ ∈ δ
a✝ : ℕ
ℓ : TP (·a✝)
δ_in : δ ∈ P (·a✝) ℓ
⊢ if isAtomic (·a✝) = true then γ = ·a✝
  else
    if isStar (·a✝) = true then lengthOfProgram γ ≤ lengthOfProgram (·a✝) else lengthOfProgram γ < lengthOfProgram (·a✝)

case sequence
γ : Program
δ : List Program
γ_in : γ ∈ δ
a✝¹ a✝ : Program
ℓ : TP (a✝¹;'a✝)
δ_in : δ ∈ P (a✝¹;'a✝) ℓ
⊢ if isAtomic (a✝¹;'a✝) = true then γ = (a✝¹;'a✝)
  else
    if isStar (a✝¹;'a✝) = true then lengthOfProgram γ ≤ lengthOfProgram (a✝¹;'a✝)
    else lengthOfProgram γ < lengthOfProgram (a✝¹;'a✝)

case union
γ : Program
δ : List Program
γ_in : γ ∈ δ
a✝¹ a✝ : Program
ℓ : TP (a✝¹⋓a✝)
δ_in : δ ∈ P (a✝¹⋓a✝) ℓ
⊢ if isAtomic (a✝¹⋓a✝) = true then γ = (a✝¹⋓a✝)
  else
    if isStar (a✝¹⋓a✝) = true then lengthOfProgram γ ≤ lengthOfProgram (a✝¹⋓a✝)
    else lengthOfProgram γ < lengthOfProgram (a✝¹⋓a✝)

case star
γ : Program
δ : List Program
γ_in : γ ∈ δ
a✝ : Program
ℓ : TP (∗a✝)
δ_in : δ ∈ P (∗a✝) ℓ
⊢ if isAtomic (∗a✝) = true then γ = (∗a✝)
  else
    if isStar (∗a✝) = true then lengthOfProgram γ ≤ lengthOfProgram (∗a✝) else lengthOfProgram γ < lengthOfProgram (∗a✝)

case test
γ : Program
δ : List Program
γ_in : γ ∈ δ
a✝ : Formula
ℓ : TP (?'a✝)
δ_in : δ ∈ P (?'a✝) ℓ
⊢ if isAtomic (?'a✝) = true then γ = (?'a✝)
  else
    if isStar (?'a✝) = true then lengthOfProgram γ ≤ lengthOfProgram (?'a✝)
    else lengthOfProgram γ < lengthOfProgram (?'a✝)
Tactic:
all_goals
  simp_all [isAtomic, isStar, P]
Proof state after:
case sequence
γ : Program
δ : List Program
γ_in : γ ∈ δ
a✝¹ a✝ : Program
ℓ : TP (a✝¹;'a✝)
δ_in :
  (∃ a ∈ List.filter (fun x => x != []) (P a✝¹ fun τ => ℓ ⟨↑τ, ⋯⟩), a ++ [a✝] = δ) ∨
    δ ∈ if [] ∈ P a✝¹ fun τ => ℓ ⟨↑τ, ⋯⟩ then P a✝ fun τ => ℓ ⟨↑τ, ⋯⟩ else []
⊢ lengthOfProgram γ < 1 + lengthOfProgram a✝¹ + lengthOfProgram a✝

case union
γ : Program
δ : List Program
γ_in : γ ∈ δ
a✝¹ a✝ : Program
ℓ : TP (a✝¹⋓a✝)
δ_in : (δ ∈ P a✝¹ fun τ => ℓ ⟨↑τ, ⋯⟩) ∨ δ ∈ P a✝ fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram a✝¹ + lengthOfProgram a✝

case star
γ : Program
δ : List Program
γ_in : γ ∈ δ
a✝ : Program
ℓ : TP (∗a✝)
δ_in : δ = [] ∨ ∃ a ∈ List.filter (fun x => x != []) (P a✝ fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗a✝] = δ
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram a✝

case test
γ : Program
δ : List Program
γ_in : γ ∈ δ
a✝ : Formula
ℓ : TP (?'a✝)
δ_in : δ ∈ if ℓ ⟨a✝, ⋯⟩ = true then [[]] else []
⊢ lengthOfProgram γ < 2 + lengthOfFormula a✝
Theorem: P_goes_down
Proof state before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : (δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩) ∨ δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
case union α β =>
  cases δ_in
  case inl δ_in =>
    have IH := P_goes_down γ_in δ_in
    cases em (isAtomic α) <;> cases em (isStar α)
    all_goals (simp_all;try linarith)
  case inr δ_in =>
    have IH := P_goes_down γ_in δ_in
    cases em (isAtomic β) <;> cases em (isStar β)
    all_goals (simp_all;try linarith)
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α : Program
ℓ : TP (∗α)
δ_in : δ = [] ∨ ∃ a ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗α] = δ
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
case star α =>
  cases δ
  case nil =>
    exfalso; cases γ_in
  case cons =>
    simp_all only [false_or]
    rcases δ_in with ⟨αs, αs_in, def_δ⟩
    subst_eqs
    cases em (γ ∈ αs)
    case inl γ_in =>
      have IH := P_goes_down γ_in (List.mem_of_mem_filter αs_in)
      cases em (isAtomic α) <;> cases em (isStar α)
      all_goals (simp_all;try linarith)
    case inr γ_not_in =>
      have : γ = (∗α) := by rw [← def_δ] at γ_in; simp at γ_in; tauto
      subst_eqs
      simp
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
case test
γ : Program
δ : List Program
γ_in : γ ∈ δ
a✝ : Formula
ℓ : TP (?'a✝)
δ_in : δ ∈ P (?'a✝) ℓ
⊢ if isAtomic (?'a✝) = true then γ = (?'a✝)
  else
    if isStar (?'a✝) = true then lengthOfProgram γ ≤ lengthOfProgram (?'a✝)
    else lengthOfProgram γ < lengthOfProgram (?'a✝)
Tactic:
simp_all [isAtomic, isStar, P]
Proof state after:
case test
γ : Program
δ : List Program
γ_in : γ ∈ δ
a✝ : Formula
ℓ : TP (?'a✝)
δ_in : δ ∈ if ℓ ⟨a✝, ⋯⟩ = true then [[]] else []
⊢ lengthOfProgram γ < 2 + lengthOfFormula a✝
Theorem: P_goes_down
Proof state before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in :
  (∃ a ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩), a ++ [β] = δ) ∨
    δ ∈ if [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩ then P β fun τ => ℓ ⟨↑τ, ⋯⟩ else []
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
cases δ_in
Proof state after:
case inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
h✝ : ∃ a ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩), a ++ [β] = δ
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
h✝ : δ ∈ if [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩ then P β fun τ => ℓ ⟨↑τ, ⋯⟩ else []
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Theorem: P_goes_down
Proof state before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : ∃ a ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩), a ++ [β] = δ
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
case inl δ_in =>
  rcases δ_in with ⟨αs, αs_in, def_δ⟩
  subst def_δ
  simp_all
  cases γ_in
  case inl γ_in =>
    have IH := P_goes_down γ_in (List.mem_of_mem_filter αs_in)
    cases em (isAtomic α) <;> cases em (isStar α)
    all_goals (simp_all;try linarith)
  case inr γ_in =>
    subst γ_in
    linarith
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : ∃ a ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩), a ++ [β] = δ
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
rcases δ_in with ⟨αs, αs_in, def_δ⟩
Proof state after:
case intro.intro
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
def_δ : αs ++ [β] = δ
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Theorem: P_goes_down
Proof state before:
case intro.intro
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
def_δ : αs ++ [β] = δ
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
subst def_δ
Proof state after:
case intro.intro
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs ++ [β]
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Theorem: P_goes_down
Proof state before:
case intro.intro
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs ++ [β]
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
simp_all
Proof state after:
case intro.intro
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs ∨ γ = β
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Theorem: P_goes_down
Proof state before:
case intro.intro
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs ∨ γ = β
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
cases γ_in
Proof state after:
case intro.intro.inl
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
h✝ : γ ∈ αs
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case intro.intro.inr
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
h✝ : γ = β
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Theorem: P_goes_down
Proof state before:
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
case inl γ_in =>
  have IH := P_goes_down γ_in (List.mem_of_mem_filter αs_in)
  cases em (isAtomic α) <;> cases em (isStar α)
  all_goals (simp_all;try linarith)
Proof state after:
no goals
Theorem: P_goes_down
Proof state before:
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ = β
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
case inr γ_in =>
  subst γ_in
  linarith
Proof state after:
no goals