*** file: /net/cs/htdocs/users/goguen/kumo/revlist/list0.duck
*****************************************
style: beijing
*****************************************
spec: /net/cs/htdocs/users/goguen/kumo/revlist/list.bob
*****************************************
proof: <<RevRevThm>>
  goal: (forall L1 : List) rev(rev(L1)) = L1 .
  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: <<AppAssocThm>>
  goal: (forall L1 L2 L3 : List)
           append(append(L1, L2), L3) = append(L1, append(L2, L3)) .
  by:   induction on L1 with scheme {nil, cons};
[]
*****************************************
display: <<RevRevThm RevAppLem AppAssocThm>>
  dir: /net/cs/htdocs/groups/tatami/kumo/exs/list0
  title:  "Inductive Properties of Lists, Part 1"
  homepage: /net/cs/htdocs/users/goguen/kumo/revlist/list0.hp
  specexpl: /net/cs/htdocs/users/goguen/kumo/revlist/list.specexpl
  closing: /net/cs/htdocs/users/goguen/kumo/revlist/list0.close

  <<RevRevThm>>
  subtitle:  "The Doubly Reversed List Equation"
  expl: /net/cs/htdocs/users/goguen/kumo/revlist/list0.exp1

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

  <<AppAssocThm>>
  subtitle:  "Associativity of Append"
  expl: /net/cs/htdocs/users/goguen/kumo/revlist/list0.exp3
[]