Theorem: InterpretationPrefix
Proof state before:
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
Tactic:
any_goals
  first | apply EmptyStringPrefix | apply CharPrefix | apply PrefixAppend
Proof state after:
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 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