helphomeduck scriptspecificationfirst proof page

Duck Proof Script
Doubly Reversed Flag 


*** file: /net/cs/htdocs/users/goguen/kumo/flag/flag.duck
*****************************************
style: beijing
*****************************************
spec: /net/cs/htdocs/users/goguen/kumo/flag/flag.bob
*****************************************
relation:
   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

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

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

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