(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/LOGIC/PRed/defs".
+
(* SINGLE STEP PARALLEL REDUCTION
For cut elimination
\forall h. PRed P1 (scut (prin h) q1) S P2 q2 S
| pred_b_dx: \forall p1,p2,Q1,Q2,S. PRed Q1 p1 S Q2 p2 S \to
\forall h. PRed Q1 (scut p1 (prin h)) S Q2 p2 S
+ | pred_c : \forall p1,p2,Q1,Q2,S. PRed Q1 p1 S Q2 p2 S \to
+ \forall p. PRed Q1 (scut (impr p) (impw p1)) S Q2 p2 S
.
(*CSC: the URI must disappear: there is a bug now *)
'parred3 x1 y1 z1 x2 y2 z2 =
(cic:/matita/LOGIC/PRed/defs/PRed.ind#xpointer(1/1) x1 y1 z1 x2 y2 z2)
.
+
+notation "hvbox([a1,b1,c1] break => [a2,b2,c2])"
+ non associative with precedence 45
+for @{ 'parred3 $a1 $b1 $c1 $a2 $b2 $c2 }.