2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "lambda/par_reduction.ma".
15 inductive T : Type[0] ≝
19 | Lambda: T → T → T (* type, body *)
20 | Prod: T → T → T (* type, body *)
24 inductive red : T →T → Prop ≝
25 | rbeta: ∀P,M,N. red (App (Lambda P M) N) (M[0 ≝ N])
26 | rdapp: ∀M,N. red (App (D M) N) (D (App M N))
27 | rdlam: ∀M,N. red (Lambda M (D N)) (D (Lambda M N))
28 | rappl: ∀M,M1,N. red M M1 → red (App M N) (App M1 N)
29 | rappr: ∀M,N,N1. red N N1 → red (App M N1) (App M N1)
30 | rlaml: ∀M,M1,N. red M M1 → red (Lambda M N) (Lambda M1 N)
31 | rlamr: ∀M,N,N1. red N N1 → red(Lambda M N1) (Lambda M N1)
32 | rprodl: ∀M,M1,N. red M M1 → red (Prod M N) (Prod M1 N)
33 | rprodr: ∀M,N,N1. red N N1 → red (Prod M N1) (Prod M N1)
34 | d: ∀M,M1. red M M1 → red (D M) (D M1).
36 lemma red_to_pr: ∀M,N. red M N → pr M N.
37 #M #N #redMN (elim redMN) /2/