Theorem: InterpretationSteps (FOL/NV/Program/PEG.lean)

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
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

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
State after:
no goals

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
State after:
no goals