1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/LOGIC/PRed/defs".
17 (* SINGLE STEP PARALLEL REDUCTION
21 include "datatypes/Proof.ma".
23 inductive PRed: Proof \to Proof \to Prop \def
24 | pred_lref: \forall i. PRed (lref i) (lref i)
25 | pred_parx: \forall h. PRed (parx h) (parx h)
26 | pred_impw: \forall p1,p2. PRed p1 p2 \to PRed (impw p1) (impw p2)
27 | pred_impr: \forall p1,p2. PRed p1 p2 \to PRed (impr p1) (impr p2)
28 | pred_impi: \forall p1,p2. PRed p1 p2 \to \forall q1,q2. PRed q1 q2 \to
29 \forall r1,r2. PRed r1 r2 \to
30 PRed (impi p1 q1 r1) (impi p2 q2 r2)
31 | pred_scut: \forall p1,p2. PRed p1 p2 \to \forall q1,q2. PRed q1 q2 \to
32 PRed (scut p1 q1) (scut p2 q2)
35 (*CSC: the URI must disappear: there is a bug now *)
37 "single step parallel reduction in B->"
38 'parred x y = (cic:/matita/LOGIC/PRed/defs/PRed.ind#xpointer(1/1) x y)