Impressum scott_product.pvs   Sprache: PVS

scott_product[T1,T2:TYPE, (IMPORTING orders@product_orders)
               le1:(directed_complete_partial_order?[T1]),
               le2:(directed_complete_partial_order?[T2])]: THEORY

BEGIN

  x,y: VAR [T1,T2]

  product_order(le1:(partial_order?[T1]),
                le2:(partial_order?[T2])):
                                  (partial_order?[[T1,T2]])
    = (LAMBDA x,y: le1(x`1,y`1) & le2(x`2,y`2))

  IMPORTING scott[[T1,T2],(product_order(le1,le2))]

END scott_product