PrintForm Definitions languages Sections AutomataTheory Doc

At: lang prod sing 1 1 1

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

L(l)

By: Analyze 4

Generated subgoal:

14. i: {0...||l||}
5. L(l[0..i]) & null(l[i..||l||])
L(l)


About:
applyuniversefunctionlistprop
existsnatural_numberandassert