*** file: /net/cs/htdocs/users/goguen/kumo/list.duck
*****************************************
style: beijing
*****************************************
spec: /net/cs/htdocs/users/goguen/kumo/revlist/list.bob
*****************************************
proof: <<AppAssocThm>>
  goal: assoc-of append
***  goal: (forall L1 L2 L3 : List)
***          append(append(L1, L2), L3) = append(L1, append(L2, L3)) .
  by:   induction on sort List with scheme {nil, cons};
***  by:   induction on L1 with scheme {nil, cons};
[]
*****************************************
proof: <<RevAppLem>>
  goal: (forall L1 L2 : List)
           rev(append(L1, L2)) = append(rev(L2), rev(L1)) .
  by:   induction on L1 with scheme {nil, cons};
[]
*****************************************
proof: <<RevRevThm>>
  goal: (forall L1 : List) rev(rev(L1)) = L1 .
  by:   induction on L1 with scheme {nil, cons};
[]
*****************************************

display: <<AppAssocThm RevAppLem RevRevThm>>
  dir: /net/cs/htdocs/groups/tatami/kumo/exs/list
  title:  "Inductive Properties of Lists, Part 2"
  homepage: /net/cs/htdocs/users/goguen/kumo/revlist/list.hp
  specexpl: /net/cs/htdocs/users/goguen/kumo/revlist/list.specexpl
  closing: /net/cs/htdocs/users/goguen/kumo/revlist/list.close

  <<AppAssocThm>>
  subtitle:  "Associativity of Append"
  expl: /net/cs/htdocs/users/goguen/kumo/revlist/list.exp1

  <<RevAppLem>>
  subtitle:  "Reverse Append Lemma"
  expl: /net/cs/htdocs/users/goguen/kumo/revlist/list.exp2

  <<RevRevThm>>
  subtitle:  "The Doubly Reversed List Equation"
  expl: /net/cs/htdocs/users/goguen/kumo/revlist/list.exp3
[]