---

df-prog-equiv(A;p;q;s1,s2.R[s1; s2]) ==
  R[inl df-program-state(p) ; inl df-program-state(q) ]
   (s1:df-program-statetype(p)?. s2:df-program-statetype(q)?.
       (R[s1; s2]
        (a:A
             let s1',out1 = df-program-in-state-ap'(p;s1;a) 
             in let s2',out2 = df-program-in-state-ap'(q;s2;a) 
                in R[s1'; s2']  (out1 = out2))))

---

Definitions occuring in Statement :  df-program-in-state-ap': df-program-in-state-ap'(dfp;s;m),  df-program-state: df-program-state(dfp),  df-program-statetype: df-program-statetype(dfp),  df-program-type: df-program-type(dfp),  all: x:A. B[x],  implies: P  Q,  and: P  Q,  unit: Unit,  spread: spread def,  inl: inl x ,  union: left + right,  equal: s = t,  bag: bag(T)
Definitions :  inl: inl x ,  df-program-state: df-program-state(dfp),  union: left + right,  df-program-statetype: df-program-statetype(dfp),  unit: Unit,  implies: P  Q,  all: x:A. B[x],  spread: spread def,  df-program-in-state-ap': df-program-in-state-ap'(dfp;s;m),  and: P  Q,  equal: s = t,  bag: bag(T),  df-program-type: df-program-type(dfp)
FDL editor aliases :  df-prog-equiv

---

df-prog-equiv(A;p;q;s1,s2.R[s1;  s2])  ==
    R[inl  df-program-state(p)  ;  inl  df-program-state(q)  ]
    \mwedge{}  (\mforall{}s1:df-program-statetype(p)?.  \mforall{}s2:df-program-statetype(q)?.
              (R[s1;  s2]
              {}\mRightarrow{}  (\mforall{}a:A
                          let  s1',out1  =  df-program-in-state-ap'(p;s1;a) 
                          in  let  s2',out2  =  df-program-in-state-ap'(q;s2;a) 
                                in  R[s1';  s2']  \mwedge{}  (out1  =  out2))))


Date html generated: 2011_08_16-AM-09_36_24
Last ObjectModification: 2011_06_17-PM-01_18_05

Home Index