<?xml version="1.0" encoding="UTF-8"?>
<page xmlns="http://lambdadelta.info/"
- description = "applications of lambdadelta version 2"
- title = "applications of lambdadelta version 2"
+ description = "applications of \lambda\delta version 2"
+ title = "applications of \lambda\delta version 2"
head = "cic:/matita/lambdadelta/apps_2/ (applications of λδ version 2)"
>
<section>Contents of the Specification</section>
/3 width=5 by fpbs_strap1, fpb_fquq/
qed-.
+lemma fpbs_fqup_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ →
+ ⦃G, L, T⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+/3 width=5 by fpbs_fqus_trans, fqup_fqus/ qed-.
+
lemma fpbs_cpxs_trans: ∀h,g,G1,G,L1,L,T1,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ →
⦃G, L⦄ ⊢ T ➡*[h, g] T2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T2⦄.
#h #g #G1 #G #L1 #L #T1 #T #T2 #H1 #H @(cpxs_ind … H) -T2
/3 width=5 by fpbs_strap1, fpb_lpx/
qed-.
+lemma cpxs_fqus_fpbs: ∀h,g,G1,G2,L1,L2,T1,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T →
+ ⦃G1, L1, T⦄ ⊃* ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+/3 width=5 by fpbs_fqus_trans, cpxs_fpbs/ qed.
+
+lemma cpxs_fqup_fpbs: ∀h,g,G1,G2,L1,L2,T1,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T →
+ ⦃G1, L1, T⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+/3 width=5 by fpbs_fqup_trans, cpxs_fpbs/ qed-.
+
+lemma fqus_lpxs_fpbs: ∀h,g,G1,G2,L1,L,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L, T2⦄ →
+ ⦃G2, L⦄ ⊢ ➡*[h, g] L2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+/3 width=3 by fpbs_lpxs_trans, fqus_fpbs/ qed.
+
+lemma cpxs_fqus_lpxs_fpbs: ∀h,g,G1,G2,L1,L,L2,T1,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T →
+ ⦃G1, L1, T⦄ ⊃* ⦃G2, L, T2⦄ → ⦃G2, L⦄ ⊢ ➡*[h, g] L2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
+/3 width=5 by cpxs_fqus_fpbs, fpbs_lpxs_trans/ qed.
+
lemma fqus_fpbs_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ →
⦃G1, L1, T1⦄ ⊃* ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H @(fqus_ind_dx … H) -G1 -L1 -T1
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/computation/fpbs_alt.ma".
+
+(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************)
+
+(* Properties on extended context-sensitive parallel computation for terms **)
+
+lemma fpbs_cpxs_trans_neq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ →
+ ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → (T2 = U2 → ⊥) →
+ ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ≥[h, g] ⦃G2, L2, U2⦄.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 #HnTU2 elim (fpbs_fpbsa … H) -H
+#L0 #T0 #HT10 #H10 #HL02 elim (eq_term_dec T1 T0) [ -HT10 | -HnTU2 ]
+[ #H destruct lapply (lpxs_cpxs_trans … HTU2 … HL02) -HTU2
+ #HTU2 elim (fqus_cpxs_trans_neq … H10 … HTU2 HnTU2) -T2
+ /3 width=6 by fqus_lpxs_fpbs, ex3_intro/
+| /4 width=6 by fpbs_cpxs_trans, fqus_lpxs_fpbs, ex3_intro/
+]
+qed-.
⦃G, L2⦄ ⊢ T2 ▪[h, g] l2+1 → ⦃G, L2⦄ ⊢ T2 •[h, g] U2 →
⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, U2⦄.
/3 width=5 by fpbs_trans, cpr_lpr_fpbs, ssta_fpbs/ qed.
-
-lemma cpxs_fqup_fpbs: ∀h,g,G1,G2,L1,L2,T1,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T →
- ⦃G1, L1, T⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
-/3 width=5 by fpbs_trans, cpxs_fpbs, fqup_fpbs/ qed.
-
-lemma cpxs_fqus_fpbs: ∀h,g,G1,G2,L1,L2,T1,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T →
- ⦃G1, L1, T⦄ ⊃* ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
-/3 width=5 by fpbs_trans, cpxs_fpbs, fqus_fpbs/ qed.
-
-lemma cpxs_fqus_lpxs_fpbs: ∀h,g,G1,G2,L1,L,L2,T1,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T →
- ⦃G1, L1, T⦄ ⊃* ⦃G2, L, T2⦄ → ⦃G2, L⦄ ⊢ ➡*[h, g] L2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
-/3 width=5 by fpbs_trans, cpxs_fqus_fpbs, lpxs_fpbs/ qed.
(* *)
(**************************************************************************)
+include "basic_2/computation/fpbs_ext.ma".
+include "basic_2/computation/csx_fpbs.ma".
include "basic_2/computation/lsx_csx.ma".
include "basic_2/computation/fsb_alt.ma".
-axiom fqup_lpxs_trans_nlleq: ∀h,g,G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ →
- ∀L2. ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 → (K2 ⋕[T2, 0] L2 →⊥) →
- ∃∃L1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 &
- K1 ⋕[T1, 0] L1 → ⊥ & ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄.
-
(* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************)
(* Advanced propreties on context-senstive extended bormalizing terms *******)
-lemma csx_fsb: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⦥[h, g] T.
+lemma csx_fsb_fpbs: ∀h,g,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 →
+ ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G2, L2⦄ ⊢ ⦥[h, g] T2.
#h #g #G1 #L1 #T1 #H @(csx_ind_alt … H) -T1
-#T1 #HT1 @(csx_ind_lsx … (yinj 0) … HT1) -L1
-#L1 @(fqup_wf_ind … G1 L1 T1) -G1 -L1 -T1
-#G1 #L1 #T1 #IHu #H1 #IHl #IHc @fsb_intro
-#G2 #L2 #T2 * -G2 -L2 -T2
-[ #G2 #L2 #T2 #H12 @IHu -IHu // /2 width=5 by csx_fqup_conf/ -H1 [| -IHl ]
- [ #L0 #HL20 #HnL20 #_ elim (fqup_lpxs_trans_nlleq … H12 … HL20 HnL20) -L2
- /6 width=5 by fsb_fpbs_trans, lpxs_fpbs, fqup_fpbs, lpxs_cpxs_trans/
- | #T0 #HT20 #HnT20 elim (fqup_cpxs_trans_neq … H12 … HT20 HnT20) -T2
- /4 width=5 by fsb_fpbs_trans, fqup_fpbs/
+#T1 #HT1 #IHc #G2 #L2 #T2 @(fqup_wf_ind … G2 L2 T2) -G2 -L2 -T2
+#G0 #L0 #T0 #IHu #H10 lapply (csx_fpbs_conf … H10) // -HT1
+#HT0 generalize in match IHu; -IHu generalize in match H10; -H10
+@(lsx_ind … (csx_lsx … HT0 0)) -L0
+#L0 #_ #IHl #H10 #IHu @fsb_intro
+#G2 #L2 #T2 * -G2 -L2 -T2 [ -IHl -IHc | -IHu -IHl | ]
+[ /3 width=5 by fpbs_fqup_trans/
+| #T2 #HT02 #HnT02 elim (fpbs_cpxs_trans_neq … H10 … HT02 HnT02) -T0
+ /3 width=4 by/
+| #L2 #HL02 #HnL02 @(IHl … HL02 HnL02) -IHl -HnL02 [ -IHu -IHc | ]
+ [ /2 width=3 by fpbs_lpxs_trans/
+ | #G3 #L3 #T3 #H03 #_ elim (lpxs_fqup_trans … H03 … HL02) -L2
+ #L4 #T4 elim (eq_term_dec T0 T4) [ -IHc | -IHu ]
+ [ #H destruct /4 width=5 by fsb_fpbs_trans, lpxs_fpbs, fpbs_fqup_trans/
+ | #HnT04 #HT04 #H04 elim (fpbs_cpxs_trans_neq … H10 … HT04 HnT04) -T0
+ /4 width=8 by fpbs_fqup_trans, fpbs_lpxs_trans/
+ ]
]
-| -H1 -IHu -IHl /3 width=1 by/
-| -H1 -IHu /5 width=5 by fsb_fpbs_trans, lpxs_fpbs, lpxs_cpxs_trans/
]
qed.
+lemma csx_fsb: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⦥[h, g] T.
+/2 width=5 by csx_fsb_fpbs/ qed.
+
(* Advanced eliminators *****************************************************)
lemma csx_ind_fpbu: ∀h,g. ∀R:relation3 genv lenv term.
(* Properties on supclosure *************************************************)
+lemma lpx_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
+[ #G2 #L2 #T2 #H12 #K1 #HKL1 elim (lpx_fqu_trans … H12 … HKL1) -L1
+ /3 width=5 by cpx_cpxs, fqu_fqup, ex3_2_intro/
+| #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
+ #L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fqu_trans … H2 … HL0) -L
+ #L #T3 #HT3 #HT32 #HL2 elim (fqup_cpx_trans … HT0 … HT3) -T
+ /3 width=7 by cpxs_strap1, fqup_strap1, ex3_2_intro/
+]
+qed-.
+
+lemma lpx_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/
+#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
+#L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fquq_trans … H2 … HL0) -L
+#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpx_trans … HT0 … HT3) -T
+/3 width=7 by cpxs_strap1, fqus_strap1, ex3_2_intro/
+qed-.
+
lemma lpxs_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 →
∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2.
]
qed-.
+lemma lpxs_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2.
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(lpxs_ind_dx … H) -K1
+[ /2 width=5 by ex3_2_intro/
+| #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12
+ lapply (lpx_cpxs_trans … HT1 … HK1) -HT1
+ elim (lpx_fqup_trans … HT2 … HK1) -K
+ /3 width=7 by lpxs_strap2, cpxs_trans, ex3_2_intro/
+]
+qed-.
+
lemma lpxs_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 →
∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2.
#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpxs_trans … HT3 … HT0) -T
/3 width=7 by cpxs_trans, fqus_strap1, ex3_2_intro/
qed-.
-
-lemma lpx_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 →
- ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/
-#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
-#L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fquq_trans … H2 … HL0) -L
-#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpx_trans … HT0 … HT3) -T
-/3 width=7 by cpxs_strap1, fqus_strap1, ex3_2_intro/
-qed-.
elim (csx_fwd_flat … H) -H /3 width=1 by lsx_flat/
]
qed.
-
-(* Advanced eliminators *****************************************************)
-
-fact csx_ind_lsx_aux: ∀h,g,G,T,d. ∀R:predicate lenv.
- (∀L1. ⦃G, L1⦄ ⊢ ⬊*[h, g] T →
- (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T, d] L2 → ⊥) → R L2) →
- R L1
- ) →
- ∀L. G ⊢ ⋕⬊*[h, g, T, d] L → ⦃G, L⦄ ⊢ ⬊*[h, g] T → R L.
-#h #g #G #T #d #R #IH #L #H @(lsx_ind … H) -L
-#L1 #_ #IHL1 #HL1 @IH -IH //
-#L2 #HL12 #HnT @IHL1 -IHL1 /2 width=3 by csx_lpxs_conf/
-qed-.
-
-lemma csx_ind_lsx: ∀h,g,G,T,d. ∀R:predicate lenv.
- (∀L1. ⦃G, L1⦄ ⊢ ⬊*[h, g] T →
- (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T, d] L2 → ⊥) → R L2) →
- R L1
- ) →
- ∀L. ⦃G, L⦄ ⊢ ⬊*[h, g] T → R L.
-#h #g #G #T #d #R #IH #L #HL @(csx_ind_lsx_aux … d … HL) /4 width=1 by csx_lsx/
-qed-.
<?xml version="1.0" encoding="UTF-8"?>
<page xmlns="http://lambdadelta.info/"
- description = "lambdadelta version 2"
- title = "lambdadelta version 2"
+ description = "\lambda\delta version 2"
+ title = "\lambda\delta version 2"
head = "cic:/matita/lambdadelta/basic_2/ (λδ version 2)"
>
<section>System's Syntax and Behavior</section>
[ "fpbg ( ⦃?,?,?⦄ >⋕[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fpns" + "fpbg_fpbg" * ]
[ "fpbc ( ⦃?,?,?⦄ ≻⋕[?,?] ⦃?,?,?⦄ )" "fpbc_fpns" + "fpbc_fpbs" * ]
[ "fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpbu_lift" + "fpbu_fpns" * ]
- [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_aaa" + "fpbs_fpns" + "fpbs_fpbs" * ]
+ [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_aaa" + "fpbs_fpns" + "fpbs_fpbs" + "fpbs_ext" * ]
}
]
[ { "parallel computation for \"big tree\" normal forms" * } {
<?xml version="1.0" encoding="UTF-8"?>
<page xmlns="http://lambdadelta.info/"
- description = "lambdadelta version 2"
- title = "lambdadelta version 2"
+ description = "background for \lambda\delta version 2"
+ title = "background for \lambda\delta version 2"
head = "cic:/matita/lambdadelta/ground_2/ (background for λδ version 2)"
>
<section>Summary of the Specification</section>
projects / helm.git / commitdiff