1 | ls ~ [hd(ls) / tl(ls)] |
2 | 16. f: reduce(s,m. [[s]] rhom;Prop;[hd(ls) / tl(ls)]) 17. ||ls|| = ||v||+1 18. i:. i < ||v||+1 ls[i] term_types(ds;st1;de;[u / v][i]) 19. ls:SimpleType List, f:reduce(s,m. [[s]] rhom;Prop;ls). ||ls|| = ||v|| & (i:. i < ||v|| ls[i] term_types(ds;st1;de;v[i])) list_accum(x,t.x([[t]] e1 s s' a tr);f;v) Prop 20. f:reduce(s,m. [[s]] rhom;Prop;tl(ls)). ||tl(ls)|| = ||v|| & (i:. i < ||v|| tl(ls)[i] term_types(ds;st1;de;v[i])) list_accum(x,t.x([[t]] e1 s s' a tr);f;v) Prop f([[u]] e1 s s' a tr) reduce(s,m. [[s]] rhom;Prop;tl(ls)) |
About: