internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree
Proof state before:
F : Formula
v t : VarName
h1 : ¬v = t
⊢ ¬isFreeIn v (fastReplaceFree v t F)
Tactic:
induction F
Proof state after:
case pred_const_
v t : VarName
h1 : ¬v = t
a✝¹ : PredName
a✝ : List VarName
⊢ ¬isFreeIn v (fastReplaceFree v t (pred_const_ a✝¹ a✝))

case pred_var_
v t : VarName
h1 : ¬v = t
a✝¹ : PredName
a✝ : List VarName
⊢ ¬isFreeIn v (fastReplaceFree v t (pred_var_ a✝¹ a✝))

case eq_
v t : VarName
h1 : ¬v = t
a✝¹ a✝ : VarName
⊢ ¬isFreeIn v (fastReplaceFree v t (eq_ a✝¹ a✝))

case true_
v t : VarName
h1 : ¬v = t
⊢ ¬isFreeIn v (fastReplaceFree v t true_)

case false_
v t : VarName
h1 : ¬v = t
⊢ ¬isFreeIn v (fastReplaceFree v t false_)

case not_
v t : VarName
h1 : ¬v = t
a✝ : Formula
a_ih✝ : ¬isFreeIn v (fastReplaceFree v t a✝)
⊢ ¬isFreeIn v (fastReplaceFree v t a✝.not_)

case imp_
v t : VarName
h1 : ¬v = t
a✝¹ a✝ : Formula
a_ih✝¹ : ¬isFreeIn v (fastReplaceFree v t a✝¹)
a_ih✝ : ¬isFreeIn v (fastReplaceFree v t a✝)
⊢ ¬isFreeIn v (fastReplaceFree v t (a✝¹.imp_ a✝))

case and_
v t : VarName
h1 : ¬v = t
a✝¹ a✝ : Formula
a_ih✝¹ : ¬isFreeIn v (fastReplaceFree v t a✝¹)
a_ih✝ : ¬isFreeIn v (fastReplaceFree v t a✝)
⊢ ¬isFreeIn v (fastReplaceFree v t (a✝¹.and_ a✝))

case or_
v t : VarName
h1 : ¬v = t
a✝¹ a✝ : Formula
a_ih✝¹ : ¬isFreeIn v (fastReplaceFree v t a✝¹)
a_ih✝ : ¬isFreeIn v (fastReplaceFree v t a✝)
⊢ ¬isFreeIn v (fastReplaceFree v t (a✝¹.or_ a✝))

case iff_
v t : VarName
h1 : ¬v = t
a✝¹ a✝ : Formula
a_ih✝¹ : ¬isFreeIn v (fastReplaceFree v t a✝¹)
a_ih✝ : ¬isFreeIn v (fastReplaceFree v t a✝)
⊢ ¬isFreeIn v (fastReplaceFree v t (a✝¹.iff_ a✝))

case forall_
v t : VarName
h1 : ¬v = t
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ¬isFreeIn v (fastReplaceFree v t a✝)
⊢ ¬isFreeIn v (fastReplaceFree v t (forall_ a✝¹ a✝))

case exists_
v t : VarName
h1 : ¬v = t
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ¬isFreeIn v (fastReplaceFree v t a✝)
⊢ ¬isFreeIn v (fastReplaceFree v t (exists_ a✝¹ a✝))

case def_
v t : VarName
h1 : ¬v = t
a✝¹ : DefName
a✝ : List VarName
⊢ ¬isFreeIn v (fastReplaceFree v t (def_ a✝¹ a✝))
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree
Proof state before:
v t : VarName
h1 : ¬v = t
X : DefName
xs : List VarName
⊢ v ∉ List.map (fun x => if v = x then t else x) xs
Tactic:
case pred_const_ X xs | pred_var_ X xs | def_ X xs =>
  simp
  intro x
  split_ifs <;> tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree
Proof state before:
v t : VarName
h1 : ¬v = t
x y : VarName
⊢ ¬((v = if v = x then t else x) ∨ v = if v = y then t else y)
Tactic:
case eq_ x y =>
  split_ifs <;> tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree
Proof state before:
v t : VarName
h1 : ¬v = t
⊢ ¬False
Tactic:
case true_ | false_ =>
  simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree
Proof state before:
v t : VarName
h1 : ¬v = t
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
⊢ ¬isFreeIn v (fastReplaceFree v t phi)
Tactic:
case not_ phi phi_ih =>
  exact phi_ih
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree
Proof state before:
v t : VarName
h1 : ¬v = t
phi psi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
psi_ih : ¬isFreeIn v (fastReplaceFree v t psi)
⊢ ¬(isFreeIn v (fastReplaceFree v t phi) ∨ isFreeIn v (fastReplaceFree v t psi))
Tactic:
case
    imp_ phi psi phi_ih psi_ih
  | and_ phi psi phi_ih psi_ih
  | or_ phi psi phi_ih psi_ih
  | iff_ phi psi phi_ih psi_ih =>
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree
Proof state before:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
⊢ ¬isFreeIn v (fastReplaceFree v t (exists_ x phi))
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp only [fastReplaceFree]
  split_ifs
  case pos c1 =>
    simp only [isFreeIn]
    simp
    intro a1
    contradiction
  case neg c1 =>
    simp only [isFreeIn]
    simp
    intro _
    exact phi_ih
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree
Proof state before:
case def_
v t : VarName
h1 : ¬v = t
a✝¹ : DefName
a✝ : List VarName
⊢ ¬isFreeIn v (fastReplaceFree v t (def_ a✝¹ a✝))
Tactic:
simp only [fastReplaceFree]
Proof state after:
case def_
v t : VarName
h1 : ¬v = t
a✝¹ : DefName
a✝ : List VarName
⊢ ¬isFreeIn v (def_ a✝¹ (List.map (fun x => if v = x then t else x) a✝))
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree
Proof state before:
case def_
v t : VarName
h1 : ¬v = t
a✝¹ : DefName
a✝ : List VarName
⊢ ¬isFreeIn v (def_ a✝¹ (List.map (fun x => if v = x then t else x) a✝))
Tactic:
simp only [isFreeIn]
Proof state after:
case def_
v t : VarName
h1 : ¬v = t
a✝¹ : DefName
a✝ : List VarName
⊢ v ∉ List.map (fun x => if v = x then t else x) a✝
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree
Proof state before:
v t : VarName
h1 : ¬v = t
X : DefName
xs : List VarName
⊢ v ∉ List.map (fun x => if v = x then t else x) xs
Tactic:
simp
Proof state after:
v t : VarName
h1 : ¬v = t
X : DefName
xs : List VarName
⊢ ∀ x ∈ xs, ¬(if v = x then t else x) = v
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree
Proof state before:
v t : VarName
h1 : ¬v = t
X : DefName
xs : List VarName
⊢ ∀ x ∈ xs, ¬(if v = x then t else x) = v
Tactic:
intro x
Proof state after:
v t : VarName
h1 : ¬v = t
X : DefName
xs : List VarName
x : VarName
⊢ x ∈ xs → ¬(if v = x then t else x) = v
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree
Proof state before:
v t : VarName
h1 : ¬v = t
X : DefName
xs : List VarName
x : VarName
⊢ x ∈ xs → ¬(if v = x then t else x) = v
Tactic:
split_ifs <;> tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree
Proof state before:
v t : VarName
h1 : ¬v = t
x y : VarName
⊢ ¬((v = if v = x then t else x) ∨ v = if v = y then t else y)
Tactic:
split_ifs <;> tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree
Proof state before:
v t : VarName
h1 : ¬v = t
⊢ ¬False
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree
Proof state before:
v t : VarName
h1 : ¬v = t
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
⊢ ¬isFreeIn v (fastReplaceFree v t phi)
Tactic:
exact phi_ih
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree
Proof state before:
v t : VarName
h1 : ¬v = t
phi psi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
psi_ih : ¬isFreeIn v (fastReplaceFree v t psi)
⊢ ¬(isFreeIn v (fastReplaceFree v t phi) ∨ isFreeIn v (fastReplaceFree v t psi))
Tactic:
tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree
Proof state before:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
⊢ ¬isFreeIn v (fastReplaceFree v t (exists_ x phi))
Tactic:
simp only [fastReplaceFree]
Proof state after:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
⊢ ¬isFreeIn v (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi))
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree
Proof state before:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
⊢ ¬isFreeIn v (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi))
Tactic:
split_ifs
Proof state after:
case pos
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
h✝ : v = x
⊢ ¬isFreeIn v (exists_ x phi)

case neg
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
h✝ : ¬v = x
⊢ ¬isFreeIn v (exists_ x (fastReplaceFree v t phi))
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree
Proof state before:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 : v = x
⊢ ¬isFreeIn v (exists_ x phi)
Tactic:
case pos c1 =>
  simp only [isFreeIn]
  simp
  intro a1
  contradiction
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree
Proof state before:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 : ¬v = x
⊢ ¬isFreeIn v (exists_ x (fastReplaceFree v t phi))
Tactic:
case neg c1 =>
  simp only [isFreeIn]
  simp
  intro _
  exact phi_ih
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree
Proof state before:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 : v = x
⊢ ¬isFreeIn v (exists_ x phi)
Tactic:
simp only [isFreeIn]
Proof state after:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 : v = x
⊢ ¬(¬v = x ∧ isFreeIn v phi)
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree
Proof state before:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 : v = x
⊢ ¬(¬v = x ∧ isFreeIn v phi)
Tactic:
simp
Proof state after:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 : v = x
⊢ ¬v = x → ¬isFreeIn v phi
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree
Proof state before:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 : v = x
⊢ ¬v = x → ¬isFreeIn v phi
Tactic:
intro a1
Proof state after:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 : v = x
a1 : ¬v = x
⊢ ¬isFreeIn v phi
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree
Proof state before:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 : v = x
a1 : ¬v = x
⊢ ¬isFreeIn v phi
Tactic:
contradiction
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree
Proof state before:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 : ¬v = x
⊢ ¬isFreeIn v (exists_ x (fastReplaceFree v t phi))
Tactic:
simp only [isFreeIn]
Proof state after:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 : ¬v = x
⊢ ¬(¬v = x ∧ isFreeIn v (fastReplaceFree v t phi))
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree
Proof state before:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 : ¬v = x
⊢ ¬(¬v = x ∧ isFreeIn v (fastReplaceFree v t phi))
Tactic:
simp
Proof state after:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 : ¬v = x
⊢ ¬v = x → ¬isFreeIn v (fastReplaceFree v t phi)
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree
Proof state before:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 : ¬v = x
⊢ ¬v = x → ¬isFreeIn v (fastReplaceFree v t phi)
Tactic:
intro _
Proof state after:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 a✝ : ¬v = x
⊢ ¬isFreeIn v (fastReplaceFree v t phi)
Theorem: FOL.NV.Sub.Var.One.Rec.not_isFreeIn_fastReplaceFree
Proof state before:
v t : VarName
h1 : ¬v = t
x : VarName
phi : Formula
phi_ih : ¬isFreeIn v (fastReplaceFree v t phi)
c1 a✝ : ¬v = x
⊢ ¬isFreeIn v (fastReplaceFree v t phi)
Tactic:
exact phi_ih
Proof state after:
no goals
Theorem: InterpretationEmpty
Proof state before:
V_N V_T : Type
R : V_N → PE V_N V_T
n : ℕ
xs : List V_T
o : Option (List V_T)
h1 : Interpretation V_N V_T R (empty, xs) (n, o)
⊢ n = 1 ∧ o = some []
Tactic:
cases h1
Proof state after:
case empty
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
⊢ 1 = 1 ∧ some [] = some []
Theorem: InterpretationEmpty
Proof state before:
case empty
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
⊢ 1 = 1 ∧ some [] = some []
Tactic:
simp
Proof state after:
no goals
Theorem: InterpretationSteps
Proof state before:
V_N V_T : Type
R : V_N → PE V_N V_T
e : PE V_N V_T
xs : List V_T
o : Option (List V_T)
n : ℕ
h1 : Interpretation V_N V_T R (e, xs) (n, o)
⊢ n > 0
Tactic:
cases h1
Proof state after:
case empty
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
⊢ 1 > 0

case terminal_success
V_N V_T : Type
R : V_N → PE V_N V_T
a✝ : V_T
xs✝ : List V_T
⊢ 1 > 0

case terminal_failure_1
V_N V_T : Type
R : V_N → PE V_N V_T
a✝¹ b✝ : V_T
xs✝ : List V_T
a✝ : ¬a✝¹ = b✝
⊢ 1 > 0

case terminal_failure_2
V_N V_T : Type
R : V_N → PE V_N V_T
a✝ : V_T
xs✝ : List V_T
⊢ 1 > 0

case nonTerminal
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
o : Option (List V_T)
A✝ : V_N
n✝ : ℕ
a✝ : Interpretation V_N V_T R (R A✝, xs) (n✝, o)
⊢ n✝ + 1 > 0

case seq_success
V_N V_T : Type
R : V_N → PE V_N V_T
e1✝ e2✝ : PE V_N V_T
xs_1✝ xs_2✝ ys✝ : List V_T
n1✝ n2✝ : ℕ
a✝¹ : Interpretation V_N V_T R (e1✝, xs_1✝ ++ xs_2✝ ++ ys✝) (n1✝, some xs_1✝)
a✝ : Interpretation V_N V_T R (e2✝, xs_2✝ ++ ys✝) (n2✝, some xs_2✝)
⊢ n1✝ + n2✝ + 1 > 0

case seq_failure_1
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
e1✝ e2✝ : PE V_N V_T
n✝ : ℕ
a✝ : Interpretation V_N V_T R (e1✝, xs) (n✝, none)
⊢ n✝ + 1 > 0

case seq_failure_2
V_N V_T : Type
R : V_N → PE V_N V_T
e1✝ e2✝ : PE V_N V_T
xs✝ ys✝ : List V_T
n1✝ n2✝ : ℕ
a✝¹ : Interpretation V_N V_T R (e1✝, xs✝ ++ ys✝) (n1✝, some xs✝)
a✝ : Interpretation V_N V_T R (e2✝, ys✝) (n2✝, none)
⊢ n1✝ + n2✝ + 1 > 0

case choice_1
V_N V_T : Type
R : V_N → PE V_N V_T
e1✝ e2✝ : PE V_N V_T
xs✝ ys✝ : List V_T
n✝ : ℕ
a✝ : Interpretation V_N V_T R (e1✝, xs✝ ++ ys✝) (n✝, some xs✝)
⊢ n✝ + 1 > 0

case choice_2
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
o : Option (List V_T)
e1✝ e2✝ : PE V_N V_T
n1✝ n2✝ : ℕ
a✝¹ : Interpretation V_N V_T R (e1✝, xs) (n1✝, none)
a✝ : Interpretation V_N V_T R (e2✝, xs) (n2✝, o)
⊢ n1✝ + n2✝ + 1 > 0

case star_repetition
V_N V_T : Type
R : V_N → PE V_N V_T
e✝ : PE V_N V_T
xs_1✝ xs_2✝ ys✝ : List V_T
n1✝ n2✝ : ℕ
a✝¹ : Interpretation V_N V_T R (e✝, xs_1✝ ++ xs_2✝ ++ ys✝) (n1✝, some xs_1✝)
a✝ : Interpretation V_N V_T R (e✝.star, xs_2✝ ++ ys✝) (n2✝, some xs_2✝)
⊢ n1✝ + n2✝ + 1 > 0

case star_termination
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
e✝ : PE V_N V_T
n✝ : ℕ
a✝ : Interpretation V_N V_T R (e✝, xs) (n✝, none)
⊢ n✝ + 1 > 0

case notP_1
V_N V_T : Type
R : V_N → PE V_N V_T
e✝ : PE V_N V_T
xs✝ ys✝ : List V_T
n✝ : ℕ
a✝ : Interpretation V_N V_T R (e✝, xs✝ ++ ys✝) (n✝, some xs✝)
⊢ n✝ + 1 > 0

case notP_2
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
e✝ : PE V_N V_T
n✝ : ℕ
a✝ : Interpretation V_N V_T R (e✝, xs) (n✝, none)
⊢ n✝ + 1 > 0
Theorem: InterpretationSteps
Proof state before:
case empty
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
⊢ 1 > 0

case terminal_success
V_N V_T : Type
R : V_N → PE V_N V_T
a✝ : V_T
xs✝ : List V_T
⊢ 1 > 0

case terminal_failure_1
V_N V_T : Type
R : V_N → PE V_N V_T
a✝¹ b✝ : V_T
xs✝ : List V_T
a✝ : ¬a✝¹ = b✝
⊢ 1 > 0

case terminal_failure_2
V_N V_T : Type
R : V_N → PE V_N V_T
a✝ : V_T
xs✝ : List V_T
⊢ 1 > 0

case nonTerminal
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
o : Option (List V_T)
A✝ : V_N
n✝ : ℕ
a✝ : Interpretation V_N V_T R (R A✝, xs) (n✝, o)
⊢ n✝ + 1 > 0

case seq_success
V_N V_T : Type
R : V_N → PE V_N V_T
e1✝ e2✝ : PE V_N V_T
xs_1✝ xs_2✝ ys✝ : List V_T
n1✝ n2✝ : ℕ
a✝¹ : Interpretation V_N V_T R (e1✝, xs_1✝ ++ xs_2✝ ++ ys✝) (n1✝, some xs_1✝)
a✝ : Interpretation V_N V_T R (e2✝, xs_2✝ ++ ys✝) (n2✝, some xs_2✝)
⊢ n1✝ + n2✝ + 1 > 0

case seq_failure_1
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
e1✝ e2✝ : PE V_N V_T
n✝ : ℕ
a✝ : Interpretation V_N V_T R (e1✝, xs) (n✝, none)
⊢ n✝ + 1 > 0

case seq_failure_2
V_N V_T : Type
R : V_N → PE V_N V_T
e1✝ e2✝ : PE V_N V_T
xs✝ ys✝ : List V_T
n1✝ n2✝ : ℕ
a✝¹ : Interpretation V_N V_T R (e1✝, xs✝ ++ ys✝) (n1✝, some xs✝)
a✝ : Interpretation V_N V_T R (e2✝, ys✝) (n2✝, none)
⊢ n1✝ + n2✝ + 1 > 0

case choice_1
V_N V_T : Type
R : V_N → PE V_N V_T
e1✝ e2✝ : PE V_N V_T
xs✝ ys✝ : List V_T
n✝ : ℕ
a✝ : Interpretation V_N V_T R (e1✝, xs✝ ++ ys✝) (n✝, some xs✝)
⊢ n✝ + 1 > 0

case choice_2
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
o : Option (List V_T)
e1✝ e2✝ : PE V_N V_T
n1✝ n2✝ : ℕ
a✝¹ : Interpretation V_N V_T R (e1✝, xs) (n1✝, none)
a✝ : Interpretation V_N V_T R (e2✝, xs) (n2✝, o)
⊢ n1✝ + n2✝ + 1 > 0

case star_repetition
V_N V_T : Type
R : V_N → PE V_N V_T
e✝ : PE V_N V_T
xs_1✝ xs_2✝ ys✝ : List V_T
n1✝ n2✝ : ℕ
a✝¹ : Interpretation V_N V_T R (e✝, xs_1✝ ++ xs_2✝ ++ ys✝) (n1✝, some xs_1✝)
a✝ : Interpretation V_N V_T R (e✝.star, xs_2✝ ++ ys✝) (n2✝, some xs_2✝)
⊢ n1✝ + n2✝ + 1 > 0

case star_termination
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
e✝ : PE V_N V_T
n✝ : ℕ
a✝ : Interpretation V_N V_T R (e✝, xs) (n✝, none)
⊢ n✝ + 1 > 0

case notP_1
V_N V_T : Type
R : V_N → PE V_N V_T
e✝ : PE V_N V_T
xs✝ ys✝ : List V_T
n✝ : ℕ
a✝ : Interpretation V_N V_T R (e✝, xs✝ ++ ys✝) (n✝, some xs✝)
⊢ n✝ + 1 > 0

case notP_2
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
e✝ : PE V_N V_T
n✝ : ℕ
a✝ : Interpretation V_N V_T R (e✝, xs) (n✝, none)
⊢ n✝ + 1 > 0
Tactic:
all_goals
  omega
Proof state after:
no goals
Theorem: InterpretationSteps
Proof state before:
case notP_2
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
e✝ : PE V_N V_T
n✝ : ℕ
a✝ : Interpretation V_N V_T R (e✝, xs) (n✝, none)
⊢ n✝ + 1 > 0
Tactic:
omega
Proof state after:
no goals
Theorem: EmptyStringPrefix
Proof state before:
α : Type
xs : List α
⊢ [].IsPrefix xs
Tactic:
exact List.nil_prefix xs
Proof state after:
no goals
Theorem: CharPrefix
Proof state before:
α : Type
x : α
xs : List α
⊢ [x].IsPrefix (x :: xs)
Tactic:
exact List.prefix_iff_eq_take.mpr rfl
Proof state after:
no goals
Theorem: PrefixAppend
Proof state before:
α : Type
xs ys : List α
⊢ xs.IsPrefix (xs ++ ys)
Tactic:
exact List.prefix_append xs ys
Proof state after:
no goals
Theorem: InterpretationPrefix
Proof state before:
V_N V_T : Type
R : V_N → PE V_N V_T
e : PE V_N V_T
xs ys : List V_T
n : ℕ
h1 : Interpretation V_N V_T R (e, xs) (n, some ys)
⊢ ys.IsPrefix xs
Tactic:
induction n using Nat.strongInductionOn generalizing e
Proof state after:
case ind
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
n✝ : ℕ
a✝ : ∀ m < n✝, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some ys) → ys.IsPrefix xs
e : PE V_N V_T
h1 : Interpretation V_N V_T R (e, xs) (n✝, some ys)
⊢ ys.IsPrefix xs
Theorem: InterpretationPrefix
Proof state before:
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
n : ℕ
ih : ∀ m < n, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some ys) → ys.IsPrefix xs
e : PE V_N V_T
h1 : Interpretation V_N V_T R (e, xs) (n, some ys)
⊢ ys.IsPrefix xs
Tactic:
cases h1
Proof state after:
case empty
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
ih : ∀ m < 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some []) → [].IsPrefix xs
⊢ [].IsPrefix xs

case terminal_success
V_N V_T : Type
R : V_N → PE V_N V_T
a✝ : V_T
xs✝ : List V_T
ih : ∀ m < 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, a✝ :: xs✝) (m, some [a✝]) → [a✝].IsPrefix (a✝ :: xs✝)
⊢ [a✝].IsPrefix (a✝ :: xs✝)

case nonTerminal
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
A✝ : V_N
n✝ : ℕ
ih : ∀ m < n✝ + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some ys) → ys.IsPrefix xs
a✝ : Interpretation V_N V_T R (R A✝, xs) (n✝, some ys)
⊢ ys.IsPrefix xs

case seq_success
V_N V_T : Type
R : V_N → PE V_N V_T
e1✝ e2✝ : PE V_N V_T
xs_1✝ xs_2✝ ys✝ : List V_T
n1✝ n2✝ : ℕ
a✝¹ : Interpretation V_N V_T R (e1✝, xs_1✝ ++ xs_2✝ ++ ys✝) (n1✝, some xs_1✝)
a✝ : Interpretation V_N V_T R (e2✝, xs_2✝ ++ ys✝) (n2✝, some xs_2✝)
ih :
  ∀ m < n1✝ + n2✝ + 1,
    ∀ (e : PE V_N V_T),
      Interpretation V_N V_T R (e, xs_1✝ ++ xs_2✝ ++ ys✝) (m, some (xs_1✝ ++ xs_2✝)) →
        (xs_1✝ ++ xs_2✝).IsPrefix (xs_1✝ ++ xs_2✝ ++ ys✝)
⊢ (xs_1✝ ++ xs_2✝).IsPrefix (xs_1✝ ++ xs_2✝ ++ ys✝)

case choice_1
V_N V_T : Type
R : V_N → PE V_N V_T
ys : List V_T
e1✝ e2✝ : PE V_N V_T
ys✝ : List V_T
n✝ : ℕ
a✝ : Interpretation V_N V_T R (e1✝, ys ++ ys✝) (n✝, some ys)
ih : ∀ m < n✝ + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, ys ++ ys✝) (m, some ys) → ys.IsPrefix (ys ++ ys✝)
⊢ ys.IsPrefix (ys ++ ys✝)

case choice_2
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
e1✝ e2✝ : PE V_N V_T
n1✝ n2✝ : ℕ
a✝¹ : Interpretation V_N V_T R (e1✝, xs) (n1✝, none)
ih : ∀ m < n1✝ + n2✝ + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some ys) → ys.IsPrefix xs
a✝ : Interpretation V_N V_T R (e2✝, xs) (n2✝, some ys)
⊢ ys.IsPrefix xs

case star_repetition
V_N V_T : Type
R : V_N → PE V_N V_T
e✝ : PE V_N V_T
xs_1✝ xs_2✝ ys✝ : List V_T
n1✝ n2✝ : ℕ
a✝¹ : Interpretation V_N V_T R (e✝, xs_1✝ ++ xs_2✝ ++ ys✝) (n1✝, some xs_1✝)
a✝ : Interpretation V_N V_T R (e✝.star, xs_2✝ ++ ys✝) (n2✝, some xs_2✝)
ih :
  ∀ m < n1✝ + n2✝ + 1,
    ∀ (e : PE V_N V_T),
      Interpretation V_N V_T R (e, xs_1✝ ++ xs_2✝ ++ ys✝) (m, some (xs_1✝ ++ xs_2✝)) →
        (xs_1✝ ++ xs_2✝).IsPrefix (xs_1✝ ++ xs_2✝ ++ ys✝)
⊢ (xs_1✝ ++ xs_2✝).IsPrefix (xs_1✝ ++ xs_2✝ ++ ys✝)

case star_termination
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
e✝ : PE V_N V_T
n✝ : ℕ
a✝ : Interpretation V_N V_T R (e✝, xs) (n✝, none)
ih : ∀ m < n✝ + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some []) → [].IsPrefix xs
⊢ [].IsPrefix xs

case notP_2
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
e✝ : PE V_N V_T
n✝ : ℕ
a✝ : Interpretation V_N V_T R (e✝, xs) (n✝, none)
ih : ∀ m < n✝ + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some []) → [].IsPrefix xs
⊢ [].IsPrefix xs
Theorem: InterpretationPrefix
Proof state before:
case notP_2
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
e✝ : PE V_N V_T
n✝ : ℕ
a✝ : Interpretation V_N V_T R (e✝, xs) (n✝, none)
ih : ∀ m < n✝ + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some []) → [].IsPrefix xs
⊢ [].IsPrefix xs
Tactic:
first | apply EmptyStringPrefix | apply CharPrefix | apply PrefixAppend
Proof state after:
no goals
Theorem: InterpretationPrefix
Proof state before:
case notP_2
V_N V_T : Type
R : V_N → PE V_N V_T
xs : List V_T
e✝ : PE V_N V_T
n✝ : ℕ
a✝ : Interpretation V_N V_T R (e✝, xs) (n✝, none)
ih : ∀ m < n✝ + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some []) → [].IsPrefix xs
⊢ [].IsPrefix xs
Tactic:
apply EmptyStringPrefix
Proof state after:
no goals
Theorem: InterpretationPrefix
Proof state before:
case terminal_success
V_N V_T : Type
R : V_N → PE V_N V_T
a✝ : V_T
xs✝ : List V_T
ih : ∀ m < 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, a✝ :: xs✝) (m, some [a✝]) → [a✝].IsPrefix (a✝ :: xs✝)
⊢ [a✝].IsPrefix (a✝ :: xs✝)
Tactic:
apply CharPrefix
Proof state after:
no goals
Theorem: InterpretationPrefix
Proof state before:
case star_repetition
V_N V_T : Type
R : V_N → PE V_N V_T
e✝ : PE V_N V_T
xs_1✝ xs_2✝ ys✝ : List V_T
n1✝ n2✝ : ℕ
a✝¹ : Interpretation V_N V_T R (e✝, xs_1✝ ++ xs_2✝ ++ ys✝) (n1✝, some xs_1✝)
a✝ : Interpretation V_N V_T R (e✝.star, xs_2✝ ++ ys✝) (n2✝, some xs_2✝)
ih :
  ∀ m < n1✝ + n2✝ + 1,
    ∀ (e : PE V_N V_T),
      Interpretation V_N V_T R (e, xs_1✝ ++ xs_2✝ ++ ys✝) (m, some (xs_1✝ ++ xs_2✝)) →
        (xs_1✝ ++ xs_2✝).IsPrefix (xs_1✝ ++ xs_2✝ ++ ys✝)
⊢ (xs_1✝ ++ xs_2✝).IsPrefix (xs_1✝ ++ xs_2✝ ++ ys✝)
Tactic:
apply PrefixAppend
Proof state after:
no goals
Theorem: InterpretationPrefix
Proof state before:
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
A : V_N
n : ℕ
ih : ∀ m < n + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some ys) → ys.IsPrefix xs
ih_1 : Interpretation V_N V_T R (R A, xs) (n, some ys)
⊢ ys.IsPrefix xs
Tactic:
specialize ih n _ (R A)
Proof state after:
V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
A : V_N
n : ℕ
ih : ∀ m < n + 1, ∀ (e : PE V_N V_T), Interpretation V_N V_T R (e, xs) (m, some ys) → ys.IsPrefix xs
ih_1 : Interpretation V_N V_T R (R A, xs) (n, some ys)
⊢ n < n + 1

V_N V_T : Type
R : V_N → PE V_N V_T
xs ys : List V_T
A : V_N
n : ℕ
ih_1 : Interpretation V_N V_T R (R A, xs) (n, some ys)
ih : Interpretation V_N V_T R (R A, xs) (n, some ys) → ys.IsPrefix xs
⊢ ys.IsPrefix xs