Duck Source Code:
          Doubly Reversed Flag

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

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

by: coinduction;

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

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

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

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

This page was generated by Kumo on Fri Jul 02 14:09:27 PDT 1999.