proof: <<FlagThm>>
  spec: /cse/grad/klin/obj3/flag.obj
  goal: (forall F : Flag)  rev(rev(F)) = F  .

relation:
   op _R_ : Flag Flag -> Bool .
   vars F1 F2 : Flag .
   eq F1 R F2 = up? F1 == up? F2 . 
[]

by: coinduction;
[]

*** ************************************************************
display:
   title:  "Doubly Reversed Flag"
   putdir: /net/cs/htdocs/groups/tatami/demos/flag
   gethomepage: /home/klin/he/flag.hp
   getspecexpl: /home/klin/he/flagspecexp.html

<<FlagThm>>
   subtitle: "We show that reversing a flag twice has no effect."
   getexpl:  /net/beowulf/grad/klin/he/flagexp1.html

<<FlagThm.1>>
   subtitle: "We show that <math>R</math> is a hidden <delta/>-congruence."
   getexpl:  /net/beowulf/grad/klin/he/flagexp2.html

<<FlagThm.2>>
   subtitle: "Finally we show <math>(rev rev F) R F</math>."
   getexpl: /net/beowulf/grad/klin/he/flagexp4.html 
[]