Level: Lib Thy Top: 1 2
Hypotheses:

  1. Alph :

  2. St :

  3. Auto : Automata(Alph;St)

  4. x : Alph List

  5. y : Alph List

  6. z : Alph List

  7. Auto(x) = Auto(y)

  8. u : Alph

  9. v : Alph List

  10. Auto(v @ x) = Auto(v @ y)

Conclusion:

Auto((u::v) @ x) = Auto((u::v) @ y)

Applied Tactic: RecUnfold `compute_list` 0
Generated subgoals:

1. if null((u::v) @ x) then I(Auto) else Auto Auto(tl(((u::v) @ x))) hd(((u::v) @ x)) fi = if null((u::v) @ y) then I(Auto) else Auto Auto(tl(((u::v) @ y))) hd(((u::v) @ y)) fi