entuctive_set是否只能表达情况所处的情况，而不是为此失败？

Question

type_synonym ('q,'a) LTS = "('q * 'a set * 'q) set"

inductive LTS_is_reachable :: "('q, 'a) LTS ⇒  ('q * 'q) set ⇒ 'q ⇒ 'a list ⇒ 'q ⇒ bool" for Δ and Δ' where
  LTS_Empty[intro!]: "LTS_is_reachable Δ Δ' q [] q" |
  LTS_Step1: "LTS_is_reachable Δ Δ' q l q'" if "(q, q'') ∈ Δ'" and "LTS_is_reachable Δ Δ' q'' l q'" |
  LTS_Step2[intro!]: "LTS_is_reachable Δ Δ' q (a # w) q'" if "a ∈ σ" and "(q, σ, q'') ∈ Δ" and "LTS_is_reachable Δ Δ' q'' w q'"

我已经定义了一个LT来表达节点可以通过路径到达其他节点，其中δ表示具有条件的trantion，δ'表示无条件的transtion。我想给出一个引理，以表明如果“ p”无法达到“ε”，例如“€lts_is_reachableδδ”qxε”，以便在δ中添加a（q，p）也无法保持。

就像目标引理：

lemma "¬ LTS_is_reachable Δ Δ' q x ε  ⟹ ¬ LTS_is_reachable Δ ({(p,q)} ∪ Δ') p x ε"

但不能固定一样，在过渡中可能不会发生P。我想知道归纳_SET是否无法表达情况失败。因此，任何帮助将不胜感激。