Optimize multiplicity for fields

[mudathirmahgoub]

When translating

sig A {f: A -> A -> A}

No need for 2 assertions for the multiplicity constraint. The first assertion below should be removed.

; field (this/A <: f) multiplicity
(assert 
 (forall ((a.4 Atom)) 
   (let (
    (|this | 
     (mkTuple a.4))) 
     (=> 
       (member |this | |this/A |; this/A
        ) 
       (let (
        (|$s$ | 
         (join 
           (singleton |this |) |this/A/f |; field (this/A <: f)
          ))) 
         (subset |$s$ |; $s$
           
           (product |this/A |; this/A
             
             (product |this/A |; this/A
               |this/A |; this/A
              ))))))))


; field (this/A <: f) subset
(assert 
 (subset |this/A/f |; field (this/A <: f)
   
   (product |this/A |; this/A
     
     (product |this/A |; this/A
       
       (product |this/A |; this/A
         |this/A |; this/A
        )))))