PrintForm Definitions languages Sections AutomataTheory Doc

At: lang sing prod 1 1 1 1

1. Alph: Type
2. L: Alph*Prop
3. l: Alph*
4. i: {0...||l||}
5. null(l[0..i]) & L(l[i..||l||])

L(l)

By: Analyze 5

Generated subgoal:

15. null(l[0..i])
6. L(l[i..||l||])
L(l)


About:
applyuniversefunctionlistpropnatural_numberandassert