Menu
▾
▴
#64 Miss ′ in the conversion BoxOffice′
open
nobody
None
5
2009-06-05
2009-06-05
Anonymous
No
─ section specdebug parents standard_toolkit
└
─ [ Seat , Customer ]
└
┌ BoxOffice
seating : ℙ Seat
sold : Seat ⇸ Customer
|
dom sold ⊆ seating
└
┌ BoxOffice′
seating′ : ℙ Seat
sold′ : Seat ⇸ Customer
|
dom sold′ ⊆ seating′
└
This specification describes ...
----------------------------------------------------------------
Conversion
----------------------------------------------------------------
─ section specdebug parents standard_toolkit
└
─ [ Seat , Customer ]
└
┌ BoxOffice
seating : ℙ Seat
sold : Seat ⇸ Customer
|
dom sold ⊆ seating
└
┌ BoxOffice
seating′ : ℙ Seat
sold′ : Seat ⇸ Customer
|
dom sold′ ⊆ seating′
└
This specification describes ...
--------------------------------------
Miss ′ in the conversion BoxOffice′
