Next: UNION Up: The Rules Previous: LESS

# LIST

rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* formation . H >> ext A list by intro list
* >> ext A

. H >> A list in by intro
* >> A in

rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* canonical . H >> A list ext nil by intro nil at
* >> A in

. H >> nil in A list by intro at
* >> A in

. H >> A list ext h.t by intro .
* >> A ext h
* >> A list ext t

. H >> in A list by intro
* >> a in A
* >> b in A list

rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* noncanonical . H,x:A list, >> T ext list_ind(x;;u,v,w.)
* by elim x new w,u[,v]
* >> T[nil/x] ext
* u:A,v:A list,w:T[v/x]

>> T[/x] ext

. H >> list_ind(e;;) in T[e/z]
* by intro [over ] using A list [new u,v,w]
* >> e in A list
* >> in T[nil/z]
* u:A,v:A list,w:T[v/z]
* >> [u,v,w/x,y,z] in T[u.v/z]

rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

* computation

. H >> list_ind(nil;;) = t in T by reduce 1
* >> = t in T

. H >> list_ind(;;) = t in T by reduce 1
* >> [a,b,list_ind(b;;)/u,v,w]

= t in T

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995