helphomeduck scriptspecificationfirst proof page

Duck Proof Script
Doubly Reversed Flag

*** file: /net/cs/htdocs/users/goguen/kumo/flag/
style: beijing
spec: /net/cs/htdocs/users/goguen/kumo/flag/flag.bob
   op _R_ : Flag Flag -> Bool .
   vars F1 F2 : Flag .
   eq F1 R F2 = up? F1 == up? F2 .

proof: <<FlagThm>>
  goal: (forall F : Flag)  rev(rev(F)) = F  .
  by: ex-coind; []

display: <<FlagThm>>
   title:  "Doubly Reversed Flag"
   dir: /net/cs/htdocs/groups/tatami/kumo/exs/flag
   homepage: /net/cs/htdocs/users/goguen/kumo/flag/home
   specexpl: /net/cs/htdocs/users/goguen/kumo/flag/spec-exp
   closing:  /net/cs/htdocs/users/goguen/kumo/flag/close

   intro: "We show that reversing a flag twice has no effect."
   expl:  /net/cs/htdocs/users/goguen/kumo/flag/exp1

   intro: "We show that <math>R</math> is a hidden <delta/>-congruence."
   expl:  /net/cs/htdocs/users/goguen/kumo/flag/exp2

   intro: "Finally we show <math>(rev rev F) R F</math>."
   expl: /net/cs/htdocs/users/goguen/kumo/flag/exp4