NFAのtrace

NFAのdebugは難しい

そこで、n step 目でありえる状態の集合を表示したい

なんだが、状態の集合全体の List がないと表示は難しい。状態が有限だったら、必ず、そういうList はある

    NNtrace : { Q : Set } { Σ : Set  } 
        → NAutomaton Q  Σ
        → (all-states : List Q )
        → (exists : ( Q → Bool ) → Bool)
        → (Nstart : Q → Bool) → List  Σ → ℕ → List Q

という型の関数を作って、n step 目でありえる状態の集合をListで返せ。