PrintForm Definitions languages Sections AutomataTheory Doc

At: lang prod sing 1 1 1 1

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

L(l)

By: Analyze 5

Generated subgoal:

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


About:
applyuniversefunctionlistpropnatural_numberandassert