Nuprl Lemma : parallel-class-program-eq

  ∀[X,Y:EClass(B)]. ∀[Xpr1,Xpr2:LocalClass(X)]. ∀[Ypr1,Ypr2:LocalClass(Y)].
    (Xpr1 || Ypr1 Xpr2 || Ypr2 ∈ (Id ─→ hdataflow(Info;B))) supposing 
       ((Xpr1 Xpr2 ∈ (Id ─→ hdataflow(Info;B))) and 
       (Ypr1 Ypr2 ∈ (Id ─→ hdataflow(Info;B)))) 
  supposing valueall-type(B)


Definitions occuring in Statement :  parallel-class-program: || Y local-class: LocalClass(X) eclass: EClass(A[eo; e]) Id: Id valueall-type: valueall-type(T) uimplies: supposing a uall: [x:A]. B[x] function: x:A ─→ B[x] universe: Type equal: t ∈ T hdataflow: hdataflow(A;B)
Lemmas :  parallel-class-program_wf bag_wf hdf-ap_wf iterate-hdataflow_wf es-loc_wf event-ordering+_subtype map_wf es-E_wf es-info_wf es-before_wf hdataflow_wf iff_weakening_equal all_wf equal_wf class-ap_wf local-class_wf parallel-class_wf Id_wf valueall-type_wf and_wf pi2_wf

    \mforall{}[X,Y:EClass(B)].  \mforall{}[Xpr1,Xpr2:LocalClass(X)].  \mforall{}[Ypr1,Ypr2:LocalClass(Y)].
        (Xpr1  ||  Ypr1  =  Xpr2  ||  Ypr2)  supposing  ((Xpr1  =  Xpr2)  and  (Ypr1  =  Ypr2)) 
    supposing  valueall-type(B)

Date html generated: 2015_07_22-PM-00_03_55
Last ObjectModification: 2015_02_04-PM-05_09_47

Home Index