proof: <<FlagThm>>
    spec: 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: flag
     gethomepage: flag.hp
     getspecexpl: specexp.html

  <<FlagThm>>
     subtitle: "We show that reversing a "+
               "flag twice has no effect."
     getexpl: exp1.html

  <<FlagThm.1>>
     subtitle: "We show that <math>R</math> is "+
               "a hidden <delta/>-congruence."
     getexpl: exp2.html

  <<FlagThm.2>>
     subtitle: "Finally we show "+
               "<math>(rev rev F) R F</math>."
     getexpl: exp3.html 
  []
      

The Specification of Flag

  bth FLAG is
     bsort Flag .
     bop up_ : Flag -> Flag .
     bop dn_ : Flag -> Flag .
     bop rev_ : Flag -> Flag .
     bop up?_  : Flag -> Bool .
     var F : Flag .
     eq up? up F = true . 
     eq up? dn F = false .
     eq up? rev F = not up? F .
  endb