Nuprl - Pf derive

PrintForm Definitions grammar 1 Sections AutomataTheory Doc

1. V: Type
2. T: Type
3. G: Grammar(V;T)
4. l: (V+T)*

a:((V+T)* List). l = a[0] & (i:(||a||-1). a[i] a[(i+1)]) & a[(||a||-1)] = l

By: Witness [l]

Generated subgoals:

1 [l] ((V+T)* List)

2 l = [l][0] & (i:(||[l]||-1). [l][i] [l][(i+1)]) & [l][(||[l]||-1)] = l

3 5. a: (V+T)* List
(l = a[0] & (i:(||a||-1). a[i] a[(i+1)]) & a[(||a||-1)] = l) Prop

About:

1	`[l] ((V+T)* List)`
2	`l = [l][0] & (i:(\|\|[l]\|\|-1). [l][i] [l][(i+1)]) & [l][(\|\|[l]\|\|-1)] = l`
3	5. `a:` `(V+T)* List` `(l = a[0] & (i:(\|\|a\|\|-1). a[i] a[(i+1)]) & a[(\|\|a\|\|-1)] = l) Prop`