PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: firstn lem1 1 2 2 1 1
1. T: Type
2. x:
3. 0 < x
4. as:T*. x-1 < ||as|| firstn(x-1+1;as) = (firstn(x-1;as) @ [as[(x-1)]])
5. as: T*
6. u: T
7. v: T*
8. x < ||v||+1

if 0 < x+1 u.firstn(x+1-1;v) else nil fi = (if 0 < x u.firstn(x-1;v) else nil fi @ [(u.v)[x]])
By: SplitOnConclITE
Generated subgoal:

19. 0 < x+1
u.firstn(x+1-1;v) = (if 0 < x u.firstn(x-1;v) else nil fi @ [(u.v)[x]])

About:
equallistifthenelsenatural_numberaddconssubtract
niluniverseintless_thanallimplies