From: Ferruccio Guidi Date: Mon, 25 Nov 2013 14:42:31 +0000 (+0000) Subject: - xoa: the definitions file now includes the notations file X-Git-Tag: make_still_working~1047 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=50001ac0b45a3f6376e8cbfd9200149a01d68148;hp=c559209567ff7ec5e4d3de7fef431398f9ba2559;p=helm.git - xoa: the definitions file now includes the notations file - probe: improved "list" algorithm, and bugfixed "remove" algorithm - lib/lambda: updated and bugfixed dependences to cope with new xoa - lambdadelta/ground_2: decentralized and bugfixed notation, now copes with new xoa, some refactoring --- diff --git a/matita/components/binaries/probe/matitaList.ml b/matita/components/binaries/probe/matitaList.ml index 9f6248c0f..22b2f91b5 100644 --- a/matita/components/binaries/probe/matitaList.ml +++ b/matita/components/binaries/probe/matitaList.ml @@ -17,17 +17,34 @@ module Y = Sys module U = NUri module US = U.UriSet +module H = HExtlib module O = Options module E = Engine -let is_obj path = - F.check_suffix path ".con.ng" || - F.check_suffix path ".ind.ng" || - F.check_suffix path ".var.ng" - +let chop_extension file = + try F.chop_extension file + with Invalid_argument("Filename.chop_extension") -> file + let src_exists path = !O.no_devel || Y.file_exists path +let is_obj base path = + if H.is_regular (F.concat base path) then + F.check_suffix path ".con.ng" || + F.check_suffix path ".ind.ng" || + F.check_suffix path ".var.ng" + else false + +let is_src base path = + H.is_regular (F.concat base path) && + F.check_suffix path ".ng" + +let is_dir base path = + H.is_dir (F.concat base path) + +let is_script devel = + src_exists (chop_extension devel ^ ".ma") + let mk_file path = if F.check_suffix path "/" then S.sub path 0 (pred (S.length path)) else path ^ ".ng" @@ -38,24 +55,25 @@ let add_obj path = O.objs := US.add (U.uri_of_string str) !O.objs let add_src devel path = - if src_exists (F.chop_extension devel ^ ".ma") then - let path = F.chop_extension path in - let str = F.concat "cic:" path ^ "/" in - O.srcs := US.add (U.uri_of_string str) !O.srcs + let path = F.chop_extension path in + let str = F.concat "cic:" path ^ "/" in + O.srcs := US.add (U.uri_of_string str) !O.srcs let add_remove base path = O.remove := F.concat base path :: !O.remove -let rec scan_entry base devel path = - if is_obj path then add_obj path else - if F.check_suffix path ".ng" then - if src_exists (F.chop_extension devel ^ ".ma") - then add_src devel path else add_remove base path - else - if src_exists devel || src_exists (devel ^ ".ma") then - let files = Y.readdir (F.concat base path) in - let map base file = scan_entry base (F.concat devel file) (F.concat path file) in - A.iter (map base) files +let rec scan_entry inner base devel path = +(* Printf.eprintf "%b %s %s%!\n" inner devel path; *) + if is_obj base path && inner then add_obj path else + if is_src base path && is_script devel then add_src devel path else + if is_dir base path && is_script devel then scan_dir true base devel path else + if is_dir base path && src_exists devel then scan_dir false base devel path else + add_remove base path + +and scan_dir inner base devel path = + let files = Y.readdir (F.concat base path) in + let map base file = scan_entry inner base (F.concat devel file) (F.concat path file) in + A.iter (map base) files let from_uri base devel uri = O.no_devel := devel = ""; @@ -65,7 +83,8 @@ let from_uri base devel uri = if protocol = "cic:" then let path = S.sub str (succ i) (S.length str - succ i) in let file = mk_file path in - if Y.file_exists (F.concat base file) then scan_entry base devel file + if Y.file_exists (F.concat base file) then + scan_entry (is_script devel) base devel file else E.missing path else E.unsupported protocol diff --git a/matita/components/binaries/probe/matitaRemove.ml b/matita/components/binaries/probe/matitaRemove.ml index 87be45521..72624f0f0 100644 --- a/matita/components/binaries/probe/matitaRemove.ml +++ b/matita/components/binaries/probe/matitaRemove.ml @@ -16,8 +16,11 @@ module U = Unix module O = Options -let remove_dir dir = - let map name = Y.remove (F.concat dir name) in +let rec remove_obj name = + try Y.remove name with Sys_error _ -> remove_dir name + +and remove_dir dir = + let map name = remove_obj (F.concat dir name) in let rec rmdir dir = U.rmdir dir; (* Sys.remove does not seem to remove empty directories *) rmdir (F.dirname dir) @@ -28,8 +31,4 @@ let remove_dir dir = end let objects () = - let map name = - Y.remove name; - remove_dir (F.chop_extension name) - in - List.iter map !O.remove + List.iter remove_obj !O.remove diff --git a/matita/components/binaries/xoa/xoa.ml b/matita/components/binaries/xoa/xoa.ml index ae5bd03ab..e4e0e7c69 100644 --- a/matita/components/binaries/xoa/xoa.ml +++ b/matita/components/binaries/xoa/xoa.ml @@ -32,6 +32,7 @@ let process conf = let ooch = L.open_out preamble (R.get_string "xoa.objects") in let noch = L.open_out preamble (R.get_string "xoa.notations") in List.iter (L.out_include ooch) (R.get_list R.string "xoa.include"); + L.out_include ooch (R.get_string "xoa.notations" ^ ".ma"); List.iter (E.generate ooch noch) (R.get_list unm_ex "xoa.ex"); List.iter (E.generate ooch noch) (R.get_list unm_or "xoa.or"); List.iter (E.generate ooch noch) (R.get_list unm_and "xoa.and"); diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index 18258ae90..6eed87bc1 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -4,14 +4,14 @@ H := @ TRIM := sed "s/ \\+$$//" XOA_CONF := ground_2/xoa.conf.xml -XOA_TARGETS := ground_2/xoa_notation.ma ground_2/xoa.ma +XOA_TARGETS := ground_2/notation/xoa_notation.ma ground_2/xoa/xoa.ma XOA_DIR := ../../../components/binaries/xoa XOA := xoa.native XOA_OPTS := ../../matita.conf.xml $(XOA_CONF) XOA2_CONF := ground_2/xoa2.conf.xml -XOA2_TARGETS := ground_2/xoa2_notation.ma ground_2/xoa2.ma +XOA2_TARGETS := ground_2/notation/xoa2_notation.ma ground_2/xoa/xoa2.ma XOA2_OPTS := ../../matita.conf.xml $(XOA2_CONF) DEP_INPUT := .depend diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma index 40f2eddc2..5ca6add44 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma @@ -46,8 +46,8 @@ inductive rtm_step: relation rtm ≝ rtm_step (mk_rtm G u E ({D, V} @ S) (+ⓛW. T)) (mk_rtm G u (E. ④{Abbr} {u, D, V}) S T) | rtm_push : ∀G,u,E,W,T. - rtm_step (mk_rtm G u E ⟠ (+ⓛW. T)) - (mk_rtm G (u + 1) (E. ④{Abst} {u, E, W}) ⟠ T) + rtm_step (mk_rtm G u E (⟠) (+ⓛW. T)) + (mk_rtm G (u + 1) (E. ④{Abst} {u, E, W}) (⟠) T) | rtm_theta : ∀G,u,E,S,V,T. rtm_step (mk_rtm G u E S (+ⓓV. T)) (mk_rtm G u (E. ④{Abbr} {u, E, V}) S T) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma index 13d69acd4..3656d36f6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma @@ -32,7 +32,7 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. [ #G #L #k #L0 #des #HL0 #X #H #L2 #HL20 >(lifts_inv_sort1 … H) -H lapply (aacr_acr … H1RP H2RP (⓪)) #HAtom - @(s4 … HAtom … ◊) // + @(s4 … HAtom … (◊)) // | #I #G #L1 #K1 #V1 #B #i #HLK1 #HKV1B #IHB #L0 #des #HL01 #X #H #L2 #HL20 lapply (aacr_acr … H1RP H2RP B) #HB elim (lifts_inv_lref1 … H) -H #i1 #Hi1 #H destruct @@ -45,7 +45,7 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. [ #K2 #HK20 #H destruct elim (lift_total V0 0 (i0 +1)) #V #HV0 elim (lifts_lift_trans … Hi0 … Hdes0 … HV10 … HV0) -HV10 #V2 #HV12 #HV2 - @(s5 … HB … ◊ … HV0 HLK2) /3 width=7/ (* uses IHB HL20 V2 HV0 *) + @(s5 … HB … (◊) … HV0 HLK2) /3 width=7 by ldrops_cons, lifts_cons/ (* Note: uses IHB HL20 V2 HV0 *) | -HLK1 -IHB -HL01 -HL20 -HK1b -Hi0 -Hdes0 #K2 #V2 #A2 #HKV2A #H1KV0A #H2KV0A #_ #H1 #H2 destruct lapply (ldrop_fwd_ldrop2 … HLK2) #HLK2b @@ -53,40 +53,40 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. lapply (aaa_mono … H2KV0A … HKV0B) #H destruct -H2KV0A -HKV0B elim (lift_total V0 0 (i0 +1)) #V3 #HV03 elim (lift_total V2 0 (i0 +1)) #V #HV2 - @(s5 … HB … ◊ … (ⓝV3.V) … HLK2) [2: /2 width=1/ ] - @(s7 … HB … ◊) [ @(s8 … HB … HKV2A) // | @(s8 … HB … H1KV0A) // ] + @(s5 … HB … (◊) … (ⓝV3.V) … HLK2) [2: /2 width=1 by lift_flat/ ] + @(s7 … HB … (◊)) [ @(s8 … HB … HKV2A) // | @(s8 … HB … H1KV0A) // ] ] | #a #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20 elim (lifts_inv_bind1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct lapply (aacr_acr … H1RP H2RP A) #HA lapply (aacr_acr … H1RP H2RP B) #HB lapply (s1 … HB) -HB #HB - @(s6 … HA … ◊ ◊) // /3 width=5/ + @(s6 … HA … (◊) (◊)) /3 width=5 by lsubc_pair, ldrops_skip, liftv_nil/ | #a #G #L #W #T #B #A #HLWB #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL02 elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct - @(aacr_abst … H1RP H2RP) [ /2 width=5/ ] + @(aacr_abst … H1RP H2RP) [ /2 width=5 by/ ] #L3 #V3 #W3 #T3 #des3 #HL32 #HW03 #HT03 #H1B #H2B elim (ldrops_lsubc_trans … H1RP H2RP … HL32 … HL02) -L2 #L2 #HL32 #HL20 - lapply (aaa_lifts … L2 W3 … (des @@ des3) … HLWB) -HLWB /2 width=3/ #HLW2B - @(IHA (L2. ⓛW3) … (des + 1 @@ des3 + 1)) -IHA /2 width=3/ /3 width=5/ + lapply (aaa_lifts … L2 W3 … (des @@ des3) … HLWB) -HLWB /2 width=3 by ldrops_trans, lifts_trans/ #HLW2B + @(IHA (L2. ⓛW3) … (des + 1 @@ des3 + 1)) -IHA /2 width=3/ /3 width=5 by lsubc_abbr, ldrops_trans, ldrops_skip/ | #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20 elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct - /3 width=10/ + /3 width=10 by ldrops_nil, lifts_nil/ | #G #L #V #T #A #_ #_ #IH1A #IH2A #L0 #des #HL0 #X #H #L2 #HL20 elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct lapply (aacr_acr … H1RP H2RP A) #HA - @(s7 … HA … ◊) /2 width=5/ + @(s7 … HA … (◊)) /2 width=5 by/ ] qed. (* Basic_1: was: sc3_arity *) lemma aacr_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) → ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L, T⦄ ϵ[RP] 〚A〛. -/2 width=8/ qed. +/2 width=8 by ldrops_nil, lifts_nil, aacr_aaa_csubc_lifts/ qed. lemma acp_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) → ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → RP G L T. #RR #RS #RP #H1RP #H2RP #G #L #T #A #HT lapply (aacr_acr … H1RP H2RP A) #HA -@(s1 … HA) /2 width=4/ +@(s1 … HA) /2 width=4 by aacr_aaa/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma index 482349b69..1b0d56c7c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma @@ -89,7 +89,7 @@ lemma acr_lifts: ∀C. S8 C → S8s C. [ #L #T1 #T2 #H #HT1 <(lifts_inv_nil … H) -H // | #L1 #L #L2 #des #d #e #_ #HL2 #IHL #T2 #T1 #H #HLT2 - elim (lifts_inv_cons … H) -H /3 width=9/ + elim (lifts_inv_cons … H) -H /3 width=9 by/ ] qed. @@ -97,7 +97,7 @@ lemma rp_lifts: ∀RR,RS,RP. acr RR RS RP (λG,L,T. RP G L T) → ∀des,G,L0,L,V,V0. ⇩*[des] L0 ≡ L → ⇧*[des] V ≡ V0 → RP G L V → RP G L0 V0. #RR #RS #RP #HRP #des #G #L0 #L #V #V0 #HL0 #HV0 #HV -@acr_lifts /width=6/ +@acr_lifts /width=6 by/ @(s8 … HRP) qed. @@ -106,8 +106,7 @@ lemma rp_liftsv_all: ∀RR,RS,RP. acr RR RS RP (λG,L,T. RP G L T) → ∀des,G,L0,L,Vs,V0s. ⇧*[des] Vs ≡ V0s → ⇩*[des] L0 ≡ L → all … (RP G L) Vs → all … (RP G L0) V0s. #RR #RS #RP #HRP #des #G #L0 #L #Vs #V0s #H elim H -Vs -V0s normalize // -#T1s #T2s #T1 #T2 #HT12 #_ #IHT2s #HL0 * #HT1 #HT1s -@conj /2 width=1/ /2 width=6 by rp_lifts/ +#T1s #T2s #T1 #T2 #HT12 #_ #IHT2s #HL0 * /3 width=6 by rp_lifts, conj/ qed. (* Basic_1: was: @@ -119,25 +118,26 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) #B #A #IHB #IHA @mk_acr normalize [ #G #L #T #H elim (cp1 … H1RP G L) #k #HK - lapply (H ? (⋆k) ? ⟠ ? ? ?) -H + lapply (H ? (⋆k) ? (⟠) ? ? ?) -H [1,3: // |2,4: skip - | @(s2 … IHB … ◊) // + | @(s2 … IHB … (◊)) // | #H @(cp3 … H1RP … k) @(s1 … IHA) // ] | #G #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #des #HB #HL0 #H elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct lapply (s1 … IHB … HB) #HV0 - @(s2 … IHA … (V0 @ V0s)) /2 width=4 by lifts_simple_dx/ /3 width=6/ + @(s2 … IHA … (V0 @ V0s)) + /3 width=13 by rp_liftsv_all, acp_lifts, cp2, lifts_simple_dx, conj/ | #a #G #L #Vs #U #T #W #HA #L0 #V0 #X #des #HB #HL0 #H elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct elim (lifts_inv_flat1 … HY) -HY #U0 #X #HU0 #HX #H destruct elim (lifts_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT0 #H destruct - @(s3 … IHA … (V0 @ V0s)) /5 width=5/ + @(s3 … IHA … (V0 @ V0s)) /5 width=5 by lifts_applv, lifts_flat, lifts_bind/ | #G #L #Vs #HVs #k #L0 #V0 #X #hdes #HB #HL0 #H elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct >(lifts_inv_sort1 … HY) -Y lapply (s1 … IHB … HB) #HV0 - @(s4 … IHA … (V0 @ V0s)) /3 width=6/ + @(s4 … IHA … (V0 @ V0s)) /3 width=6 by rp_liftsv_all, conj/ | #I #G #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #des #HB #HL0 #H elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct elim (lifts_inv_lref1 … HY) -HY #i0 #Hi0 #H destruct @@ -147,15 +147,15 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) elim (lift_total W1 0 (i0 + 1)) #W2 #HW12 elim (lifts_lift_trans … Hdes0 … HVW1 … HW12) // -Hdes0 -Hi0 #V3 #HV13 #HVW2 >(lift_mono … HV13 … HV12) in HVW2; -V3 #HVW2 - @(s5 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=4/ + @(s5 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=4 by lifts_applv/ | #G #L #V1s #V2s #HV12s #a #V #T #HA #HV #L0 #V10 #X #des #HB #HL0 #H elim (lifts_inv_applv1 … H) -H #V10s #Y #HV10s #HY #H destruct elim (lifts_inv_bind1 … HY) -HY #V0 #T0 #HV0 #HT0 #H destruct elim (lift_total V10 0 1) #V20 #HV120 elim (liftv_total 0 1 V10s) #V20s #HV120s - @(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /2 width=1/ /3 width=6 by rp_lifts/ - @(HA … (des + 1)) /2 width=1/ - [ @(s8 … IHB … HB … HV120) /2 width=1/ + @(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /3 width=6 by rp_lifts, liftv_cons/ + @(HA … (des + 1)) /2 width=1 by ldrops_skip/ + [ @(s8 … IHB … HB … HV120) /2 width=1 by ldrop_ldrop/ | @lifts_applv // elim (liftsv_liftv_trans_le … HV10s … HV120s) -V10s #V10s #HV10s #HV120s >(liftv_mono … HV12s … HV10s) -V1s // @@ -163,8 +163,8 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) | #G #L #Vs #T #W #HA #HW #L0 #V0 #X #des #HB #HL0 #H elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct elim (lifts_inv_flat1 … HY) -HY #W0 #T0 #HW0 #HT0 #H destruct - @(s7 … IHA … (V0 @ V0s)) /3 width=4/ -| /3 width=7/ + @(s7 … IHA … (V0 @ V0s)) /3 width=4 by lifts_applv/ +| /3 width=7 by ldrops_cons, lifts_cons/ ] qed. @@ -179,11 +179,11 @@ lapply (aacr_acr … H1RP H2RP A) #HCA lapply (aacr_acr … H1RP H2RP B) #HCB elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct lapply (acr_lifts … HL0 … HW0 HW) -HW [ @(s8 … HCB) ] #HW0 -@(s3 … HCA … ◊) -@(s6 … HCA … ◊ ◊) // +@(s3 … HCA … (◊)) +@(s6 … HCA … (◊) (◊)) // [ @(HA … HL0) // | lapply (s1 … HCB) -HCB #HCB - @(cp4 … H1RP) /2 width=1/ + @(cp4 … H1RP) /2 width=1 by/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma index 72ae1cd80..88486384a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma @@ -16,7 +16,7 @@ * Initial invocation: - Patience on me to gain peace and perfection! - *) -include "ground_2/star.ma". +include "ground_2/lib/star.ma". include "basic_2/notation/constructors/item0_0.ma". include "basic_2/notation/constructors/snitem2_2.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma index 2ab808305..27d019994 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground_2/list.ma". +include "ground_2/lib/list.ma". include "basic_2/notation/constructors/star_0.ma". include "basic_2/notation/constructors/dxbind2_3.ma". include "basic_2/notation/constructors/dxabbr_2.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/item.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/item.ma index b85496fa5..df330a7df 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/item.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/item.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground_2/arith.ma". +include "ground_2/lib/arith.ma". (* ITEMS ********************************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma index 24e08d151..8771d46fb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "ground_2/notation/functions/append_2.ma". include "basic_2/grammar/lenv_length.ma". (* LOCAL ENVIRONMENTS *******************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma index 1ff586359..748e5cb63 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground_2/list.ma". +include "ground_2/lib/list.ma". include "basic_2/notation/functions/snapplv_2.ma". include "basic_2/grammar/term_simple.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma index bce477f21..68b23637c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground_2/lstar.ma". +include "ground_2/lib/lstar.ma". include "basic_2/notation/relations/rdrop_4.ma". include "basic_2/grammar/lenv_length.ma". include "basic_2/grammar/cl_restricted_weight.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lift_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift_vector.ma index 482eea166..52b7861be 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lift_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift_vector.ma @@ -18,7 +18,7 @@ include "basic_2/relocation/lift.ma". (* BASIC TERM VECTOR RELOCATION *********************************************) inductive liftv (d,e:nat) : relation (list term) ≝ -| liftv_nil : liftv d e ◊ ◊ +| liftv_nil : liftv d e (◊) (◊) | liftv_cons: ∀T1s,T2s,T1,T2. ⇧[d, e] T1 ≡ T2 → liftv d e T1s T2s → liftv d e (T1 @ T1s) (T2 @ T2s) @@ -31,10 +31,10 @@ interpretation "relocation (vector)" 'RLift d e T1s T2s = (liftv d e T1s T2s). fact liftv_inv_nil1_aux: ∀T1s,T2s,d,e. ⇧[d, e] T1s ≡ T2s → T1s = ◊ → T2s = ◊. #T1s #T2s #d #e * -T1s -T2s // #T1s #T2s #T1 #T2 #_ #_ #H destruct -qed. +qed-. lemma liftv_inv_nil1: ∀T2s,d,e. ⇧[d, e] ◊ ≡ T2s → T2s = ◊. -/2 width=5/ qed-. +/2 width=5 by liftv_inv_nil1_aux/ qed-. fact liftv_inv_cons1_aux: ∀T1s,T2s,d,e. ⇧[d, e] T1s ≡ T2s → ∀U1,U1s. T1s = U1 @ U1s → @@ -42,21 +42,21 @@ fact liftv_inv_cons1_aux: ∀T1s,T2s,d,e. ⇧[d, e] T1s ≡ T2s → T2s = U2 @ U2s. #T1s #T2s #d #e * -T1s -T2s [ #U1 #U1s #H destruct -| #T1s #T2s #T1 #T2 #HT12 #HT12s #U1 #U1s #H destruct /2 width=5/ +| #T1s #T2s #T1 #T2 #HT12 #HT12s #U1 #U1s #H destruct /2 width=5 by ex3_2_intro/ ] -qed. +qed-. lemma liftv_inv_cons1: ∀U1,U1s,T2s,d,e. ⇧[d, e] U1 @ U1s ≡ T2s → ∃∃U2,U2s. ⇧[d, e] U1 ≡ U2 & ⇧[d, e] U1s ≡ U2s & T2s = U2 @ U2s. -/2 width=3/ qed-. +/2 width=3 by liftv_inv_cons1_aux/ qed-. (* Basic properties *********************************************************) lemma liftv_total: ∀d,e. ∀T1s:list term. ∃T2s. ⇧[d, e] T1s ≡ T2s. #d #e #T1s elim T1s -T1s -[ /2 width=2/ +[ /2 width=2 by liftv_nil, ex_intro/ | #T1 #T1s * #T2s #HT12s - elim (lift_total T1 d e) /3 width=2/ + elim (lift_total T1 d e) /3 width=2 by liftv_cons, ex_intro/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/sh.ma b/matita/matita/contribs/lambdadelta/basic_2/static/sh.ma index f43b9b31d..bab748f75 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/sh.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/sh.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground_2/arith.ma". +include "ground_2/lib/arith.ma". (* SORT HIERARCHY ***********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2.ma index 4cee5b104..57bb952b4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2.ma @@ -18,7 +18,7 @@ include "basic_2/grammar/term_vector.ma". (* GENERIC RELOCATION WITH PAIRS ********************************************) inductive at: list2 nat nat → relation nat ≝ -| at_nil: ∀i. at ⟠ i i +| at_nil: ∀i. at (⟠) i i | at_lt : ∀des,d,e,i1,i2. i1 < d → at des i1 i2 → at ({d, e} @ des) i1 i2 | at_ge : ∀des,d,e,i1,i2. d ≤ i1 → @@ -36,10 +36,10 @@ fact at_inv_nil_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 → des = ⟠ → i1 = | #des #d #e #i1 #i2 #_ #_ #H destruct | #des #d #e #i1 #i2 #_ #_ #H destruct ] -qed. +qed-. lemma at_inv_nil: ∀i1,i2. @⦃i1, ⟠⦄ ≡ i2 → i1 = i2. -/2 width=3/ qed-. +/2 width=3 by at_inv_nil_aux/ qed-. fact at_inv_cons_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 → ∀d,e,des0. des = {d, e} @ des0 → @@ -47,15 +47,15 @@ fact at_inv_cons_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 → d ≤ i1 ∧ @⦃i1 + e, des0⦄ ≡ i2. #des #i1 #i2 * -des -i1 -i2 [ #i #d #e #des #H destruct -| #des1 #d1 #e1 #i1 #i2 #Hid1 #Hi12 #d2 #e2 #des2 #H destruct /3 width=1/ -| #des1 #d1 #e1 #i1 #i2 #Hdi1 #Hi12 #d2 #e2 #des2 #H destruct /3 width=1/ +| #des1 #d1 #e1 #i1 #i2 #Hid1 #Hi12 #d2 #e2 #des2 #H destruct /3 width=1 by or_introl, conj/ +| #des1 #d1 #e1 #i1 #i2 #Hdi1 #Hi12 #d2 #e2 #des2 #H destruct /3 width=1 by or_intror, conj/ ] -qed. +qed-. lemma at_inv_cons: ∀des,d,e,i1,i2. @⦃i1, {d, e} @ des⦄ ≡ i2 → i1 < d ∧ @⦃i1, des⦄ ≡ i2 ∨ d ≤ i1 ∧ @⦃i1 + e, des⦄ ≡ i2. -/2 width=3/ qed-. +/2 width=3 by at_inv_cons_aux/ qed-. lemma at_inv_cons_lt: ∀des,d,e,i1,i2. @⦃i1, {d, e} @ des⦄ ≡ i2 → i1 < d → @⦃i1, des⦄ ≡ i2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2_gr2.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2_gr2.ma index 9e8ced3a8..22bf6af97 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2_gr2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2_gr2.ma @@ -22,8 +22,8 @@ theorem at_mono: ∀des,i,i1. @⦃i, des⦄ ≡ i1 → ∀i2. @⦃i, des⦄ ≡ #des #i #i1 #H elim H -des -i -i1 [ #i #x #H <(at_inv_nil … H) -x // | #des #d #e #i #i1 #Hid #_ #IHi1 #x #H - lapply (at_inv_cons_lt … H Hid) -H -Hid /2 width=1/ + lapply (at_inv_cons_lt … H Hid) -H -Hid /2 width=1 by/ | #des #d #e #i #i1 #Hdi #_ #IHi1 #x #H - lapply (at_inv_cons_ge … H Hdi) -H -Hdi /2 width=1/ + lapply (at_inv_cons_ge … H Hdi) -H -Hdi /2 width=1 by/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2_minus.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2_minus.ma index ba6dbd544..3c32514d2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2_minus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/gr2_minus.ma @@ -18,7 +18,7 @@ include "basic_2/substitution/gr2.ma". (* GENERIC RELOCATION WITH PAIRS ********************************************) inductive minuss: nat → relation (list2 nat nat) ≝ -| minuss_nil: ∀i. minuss i ⟠ ⟠ +| minuss_nil: ∀i. minuss i (⟠) (⟠) | minuss_lt : ∀des1,des2,d,e,i. i < d → minuss i des1 des2 → minuss i ({d, e} @ des1) ({d - i, e} @ des2) | minuss_ge : ∀des1,des2,d,e,i. d ≤ i → minuss (e + i) des1 des2 → @@ -36,10 +36,10 @@ fact minuss_inv_nil1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 → des1 = ⟠ → | #des1 #des2 #d #e #i #_ #_ #H destruct | #des1 #des2 #d #e #i #_ #_ #H destruct ] -qed. +qed-. lemma minuss_inv_nil1: ∀des2,i. ⟠ ▭ i ≡ des2 → des2 = ⟠. -/2 width=4/ qed-. +/2 width=4 by minuss_inv_nil1_aux/ qed-. fact minuss_inv_cons1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 → ∀d,e,des. des1 = {d, e} @ des → @@ -48,16 +48,16 @@ fact minuss_inv_cons1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 → des2 = {d - i, e} @ des0. #des1 #des2 #i * -des1 -des2 -i [ #i #d #e #des #H destruct -| #des1 #des #d1 #e1 #i1 #Hid1 #Hdes #d2 #e2 #des2 #H destruct /3 width=3/ -| #des1 #des #d1 #e1 #i1 #Hdi1 #Hdes #d2 #e2 #des2 #H destruct /3 width=1/ +| #des1 #des #d1 #e1 #i1 #Hid1 #Hdes #d2 #e2 #des2 #H destruct /3 width=3 by ex3_intro, or_intror/ +| #des1 #des #d1 #e1 #i1 #Hdi1 #Hdes #d2 #e2 #des2 #H destruct /3 width=1 by or_introl, conj/ ] -qed. +qed-. lemma minuss_inv_cons1: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 → d ≤ i ∧ des1 ▭ e + i ≡ des2 ∨ ∃∃des. i < d & des1 ▭ i ≡ des & des2 = {d - i, e} @ des. -/2 width=3/ qed-. +/2 width=3 by minuss_inv_cons1_aux/ qed-. lemma minuss_inv_cons1_ge: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 → d ≤ i → des1 ▭ e + i ≡ des2. @@ -70,8 +70,7 @@ qed-. lemma minuss_inv_cons1_lt: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 → i < d → ∃∃des. des1 ▭ i ≡ des & des2 = {d - i, e} @ des. -#des1 #des2 #d #e #i #H -elim (minuss_inv_cons1 … H) -H * /2 width=3/ #Hdi #_ #Hid -lapply (lt_to_le_to_lt … Hid Hdi) -Hid -Hdi #Hi -elim (lt_refl_false … Hi) +#des1 #des2 #d #e #i #H elim (minuss_inv_cons1 … H) -H * /2 width=3 by ex2_intro/ +#Hdi #_ #Hid lapply (lt_to_le_to_lt … Hid Hdi) -Hid -Hdi +#Hi elim (lt_refl_false … Hi) qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma index 069f632f4..912487a44 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma @@ -20,7 +20,7 @@ include "basic_2/substitution/lifts.ma". (* GENERIC LOCAL ENVIRONMENT SLICING ****************************************) inductive ldrops: list2 nat nat → relation lenv ≝ -| ldrops_nil : ∀L. ldrops ⟠ L L +| ldrops_nil : ∀L. ldrops (⟠) L L | ldrops_cons: ∀L1,L,L2,des,d,e. ldrops des L1 L → ⇩[d,e] L ≡ L2 → ldrops ({d, e} @ des) L1 L2 . @@ -33,11 +33,11 @@ interpretation "generic local environment slicing" fact ldrops_inv_nil_aux: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → des = ⟠ → L1 = L2. #L1 #L2 #des * -L1 -L2 -des // #L1 #L #L2 #d #e #des #_ #_ #H destruct -qed. +qed-. (* Basic_1: was: drop1_gen_pnil *) lemma ldrops_inv_nil: ∀L1,L2. ⇩*[⟠] L1 ≡ L2 → L1 = L2. -/2 width=3/ qed-. +/2 width=3 by ldrops_inv_nil_aux/ qed-. fact ldrops_inv_cons_aux: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → ∀d,e,tl. des = {d, e} @ tl → @@ -45,13 +45,13 @@ fact ldrops_inv_cons_aux: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → #L1 #L2 #des * -L1 -L2 -des [ #L #d #e #tl #H destruct | #L1 #L #L2 #des #d #e #HT1 #HT2 #hd #he #tl #H destruct - /2 width=3/ -qed. + /2 width=3 by ex2_intro/ +qed-. (* Basic_1: was: drop1_gen_pcons *) lemma ldrops_inv_cons: ∀L1,L2,d,e,des. ⇩*[{d, e} @ des] L1 ≡ L2 → ∃∃L. ⇩*[des] L1 ≡ L & ⇩[d, e] L ≡ L2. -/2 width=3/ qed-. +/2 width=3 by ldrops_inv_cons_aux/ qed-. lemma ldrops_inv_skip2: ∀I,des,i,des2. des ▭ i ≡ des2 → ∀L1,K2,V2. ⇩*[des2] L1 ≡ K2. ⓑ{I} V2 → @@ -61,16 +61,16 @@ lemma ldrops_inv_skip2: ∀I,des,i,des2. des ▭ i ≡ des2 → L1 = K1. ⓑ{I} V1. #I #des #i #des2 #H elim H -des -i -des2 [ #i #L1 #K2 #V2 #H - >(ldrops_inv_nil … H) -L1 /2 width=7/ + >(ldrops_inv_nil … H) -L1 /2 width=7 by lifts_nil, minuss_nil, ex4_3_intro, ldrops_nil/ | #des #des2 #d #e #i #Hid #_ #IHdes2 #L1 #K2 #V2 #H elim (ldrops_inv_cons … H) -H #L #HL1 #H - elim (ldrop_inv_skip2 … H) -H /2 width=1/ #K #V >minus_plus #HK2 #HV2 #H destruct + elim (ldrop_inv_skip2 … H) -H /2 width=1 by lt_plus_to_minus_r/ #K #V >minus_plus #HK2 #HV2 #H destruct elim (IHdes2 … HL1) -IHdes2 -HL1 #K1 #V1 #des1 #Hdes1 #HK1 #HV1 #X destruct - @(ex4_3_intro … K1 V1 … ) // [3,4: /2 width=7/ | skip ] - normalize >plus_minus // @minuss_lt // /2 width=1/ (**) (* explicit constructors, /3 width=1/ is a bit slow *) + @(ex4_3_intro … K1 V1 … ) // [3,4: /2 width=7 by lifts_cons, ldrops_cons/ | skip ] + normalize >plus_minus /3 width=1 by minuss_lt, lt_minus_to_plus/ (**) (* explicit constructors *) | #des #des2 #d #e #i #Hid #_ #IHdes2 #L1 #K2 #V2 #H elim (IHdes2 … H) -IHdes2 -H #K1 #V1 #des1 #Hdes1 #HK1 #HV1 #X destruct - /4 width=7/ + /4 width=7 by minuss_ge, ex4_3_intro, le_S_S/ ] qed-. @@ -83,7 +83,7 @@ lemma ldrops_skip: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → ∀V1,V2. ⇧*[des] V2 [ #L #V1 #V2 #HV12 #I >(lifts_inv_nil … HV12) -HV12 // | #L1 #L #L2 #des #d #e #_ #HL2 #IHL #V1 #V2 #H #I - elim (lifts_inv_cons … H) -H /3 width=5/ + elim (lifts_inv_cons … H) -H /3 width=5 by ldrop_skip, ldrops_cons/ ]. qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts.ma index 20727c4cd..31b383145 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts.ma @@ -19,7 +19,7 @@ include "basic_2/substitution/gr2_plus.ma". (* GENERIC TERM RELOCATION **************************************************) inductive lifts: list2 nat nat → relation term ≝ -| lifts_nil : ∀T. lifts ⟠ T T +| lifts_nil : ∀T. lifts (⟠) T T | lifts_cons: ∀T1,T,T2,des,d,e. ⇧[d,e] T1 ≡ T → lifts des T T2 → lifts ({d, e} @ des) T1 T2 . @@ -32,10 +32,10 @@ interpretation "generic relocation (term)" fact lifts_inv_nil_aux: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → des = ⟠ → T1 = T2. #T1 #T2 #des * -T1 -T2 -des // #T1 #T #T2 #d #e #des #_ #_ #H destruct -qed. +qed-. lemma lifts_inv_nil: ∀T1,T2. ⇧*[⟠] T1 ≡ T2 → T1 = T2. -/2 width=3/ qed-. +/2 width=3 by lifts_inv_nil_aux/ qed-. fact lifts_inv_cons_aux: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → ∀d,e,tl. des = {d, e} @ tl → @@ -43,12 +43,12 @@ fact lifts_inv_cons_aux: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → #T1 #T2 #des * -T1 -T2 -des [ #T #d #e #tl #H destruct | #T1 #T #T2 #des #d #e #HT1 #HT2 #hd #he #tl #H destruct - /2 width=3/ -qed. + /2 width=3 by ex2_intro/ +qed-. lemma lifts_inv_cons: ∀T1,T2,d,e,des. ⇧*[{d, e} @ des] T1 ≡ T2 → ∃∃T. ⇧[d, e] T1 ≡ T & ⇧*[des] T ≡ T2. -/2 width=3/ qed-. +/2 width=3 by lifts_inv_cons_aux/ qed-. (* Basic_1: was: lift1_sort *) lemma lifts_inv_sort1: ∀T2,k,des. ⇧*[des] ⋆k ≡ T2 → T2 = ⋆k. @@ -56,7 +56,7 @@ lemma lifts_inv_sort1: ∀T2,k,des. ⇧*[des] ⋆k ≡ T2 → T2 = ⋆k. [ #H <(lifts_inv_nil … H) -H // | #d #e #des #IH #H elim (lifts_inv_cons … H) -H #X #H - >(lift_inv_sort1 … H) -H /2 width=1/ + >(lift_inv_sort1 … H) -H /2 width=1 by/ ] qed-. @@ -64,11 +64,11 @@ qed-. lemma lifts_inv_lref1: ∀T2,des,i1. ⇧*[des] #i1 ≡ T2 → ∃∃i2. @⦃i1, des⦄ ≡ i2 & T2 = #i2. #T2 #des elim des -des -[ #i1 #H <(lifts_inv_nil … H) -H /2 width=3/ +[ #i1 #H <(lifts_inv_nil … H) -H /2 width=3 by at_nil, ex2_intro/ | #d #e #des #IH #i1 #H elim (lifts_inv_cons … H) -H #X #H1 #H2 elim (lift_inv_lref1 … H1) -H1 * #Hdi1 #H destruct - elim (IH … H2) -IH -H2 /3 width=3/ + elim (IH … H2) -IH -H2 /3 width=3 by at_lt, at_ge, ex2_intro/ ] qed-. @@ -77,7 +77,7 @@ lemma lifts_inv_gref1: ∀T2,p,des. ⇧*[des] §p ≡ T2 → T2 = §p. [ #H <(lifts_inv_nil … H) -H // | #d #e #des #IH #H elim (lifts_inv_cons … H) -H #X #H - >(lift_inv_gref1 … H) -H /2 width=1/ + >(lift_inv_gref1 … H) -H /2 width=1 by/ ] qed-. @@ -87,12 +87,12 @@ lemma lifts_inv_bind1: ∀a,I,T2,des,V1,U1. ⇧*[des] ⓑ{a,I} V1. U1 ≡ T2 → T2 = ⓑ{a,I} V2. U2. #a #I #T2 #des elim des -des [ #V1 #U1 #H - <(lifts_inv_nil … H) -H /2 width=5/ + <(lifts_inv_nil … H) -H /2 width=5 by ex3_2_intro, lifts_nil/ | #d #e #des #IHdes #V1 #U1 #H elim (lifts_inv_cons … H) -H #X #H #HT2 elim (lift_inv_bind1 … H) -H #V #U #HV1 #HU1 #H destruct elim (IHdes … HT2) -IHdes -HT2 #V2 #U2 #HV2 #HU2 #H destruct - /3 width=5/ + /3 width=5 by ex3_2_intro, lifts_cons/ ] qed-. @@ -102,23 +102,23 @@ lemma lifts_inv_flat1: ∀I,T2,des,V1,U1. ⇧*[des] ⓕ{I} V1. U1 ≡ T2 → T2 = ⓕ{I} V2. U2. #I #T2 #des elim des -des [ #V1 #U1 #H - <(lifts_inv_nil … H) -H /2 width=5/ + <(lifts_inv_nil … H) -H /2 width=5 by ex3_2_intro, lifts_nil/ | #d #e #des #IHdes #V1 #U1 #H elim (lifts_inv_cons … H) -H #X #H #HT2 elim (lift_inv_flat1 … H) -H #V #U #HV1 #HU1 #H destruct elim (IHdes … HT2) -IHdes -HT2 #V2 #U2 #HV2 #HU2 #H destruct - /3 width=5/ + /3 width=5 by ex3_2_intro, lifts_cons/ ] qed-. (* Basic forward lemmas *****************************************************) lemma lifts_simple_dx: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄. -#T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_dx/ +#T1 #T2 #des #H elim H -T1 -T2 -des /3 width=5 by lift_simple_dx/ qed-. lemma lifts_simple_sn: ∀T1,T2,des. ⇧*[des] T1 ≡ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄. -#T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_sn/ +#T1 #T2 #des #H elim H -T1 -T2 -des /3 width=5 by lift_simple_sn/ qed-. (* Basic properties *********************************************************) @@ -129,7 +129,7 @@ lemma lifts_bind: ∀a,I,T2,V1,V2,des. ⇧*[des] V1 ≡ V2 → #a #I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des [ #V #T1 #H >(lifts_inv_nil … H) -H // | #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H - elim (lifts_inv_cons … H) -H /3 width=3/ + elim (lifts_inv_cons … H) -H /3 width=3 by lift_bind, lifts_cons/ ] qed. @@ -139,13 +139,12 @@ lemma lifts_flat: ∀I,T2,V1,V2,des. ⇧*[des] V1 ≡ V2 → #I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des [ #V #T1 #H >(lifts_inv_nil … H) -H // | #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H - elim (lifts_inv_cons … H) -H /3 width=3/ + elim (lifts_inv_cons … H) -H /3 width=3 by lift_flat, lifts_cons/ ] qed. lemma lifts_total: ∀des,T1. ∃T2. ⇧*[des] T1 ≡ T2. -#des elim des -des /2 width=2/ -#d #e #des #IH #T1 -elim (lift_total T1 d e) #T #HT1 -elim (IH T) -IH /3 width=4/ +#des elim des -des /2 width=2 by lifts_nil, ex_intro/ +#d #e #des #IH #T1 elim (lift_total T1 d e) +#T #HT1 elim (IH T) -IH /3 width=4 by lifts_cons, ex_intro/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts_vector.ma index 7046c9d32..e86d928d7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lifts_vector.ma @@ -18,7 +18,7 @@ include "basic_2/substitution/lifts.ma". (* GENERIC TERM VECTOR RELOCATION *******************************************) inductive liftsv (des:list2 nat nat) : relation (list term) ≝ -| liftsv_nil : liftsv des ◊ ◊ +| liftsv_nil : liftsv des (◊) (◊) | liftsv_cons: ∀T1s,T2s,T1,T2. ⇧*[des] T1 ≡ T2 → liftsv des T1s T2s → liftsv des (T1 @ T1s) (T2 @ T2s) @@ -34,12 +34,12 @@ lemma lifts_inv_applv1: ∀V1s,U1,T2,des. ⇧*[des] Ⓐ V1s. U1 ≡ T2 → ∃∃V2s,U2. ⇧*[des] V1s ≡ V2s & ⇧*[des] U1 ≡ U2 & T2 = Ⓐ V2s. U2. #V1s elim V1s -V1s normalize -[ #T1 #T2 #des #HT12 - @(ex3_2_intro) [3,4: // |1,2: skip | // ] (**) (* explicit constructor *) +[ #T1 #T2 #des #HT12 + @ex3_2_intro [3,4: // |1,2: skip | // ] (**) (* explicit constructor *) | #V1 #V1s #IHV1s #T1 #X #des #H elim (lifts_inv_flat1 … H) -H #V2 #Y #HV12 #HY #H destruct elim (IHV1s … HY) -IHV1s -HY #V2s #T2 #HV12s #HT12 #H destruct - @(ex3_2_intro) [4: // |3: /2 width=2/ |1,2: skip | // ] (**) (* explicit constructor *) + @(ex3_2_intro) [4: // |3: /2 width=2 by liftsv_cons/ |1,2: skip | // ] (**) (* explicit constructor *) ] qed-. @@ -49,5 +49,5 @@ qed-. lemma lifts_applv: ∀V1s,V2s,des. ⇧*[des] V1s ≡ V2s → ∀T1,T2. ⇧*[des] T1 ≡ T2 → ⇧*[des] Ⓐ V1s. T1 ≡ Ⓐ V2s. T2. -#V1s #V2s #des #H elim H -V1s -V2s // /3 width=1/ +#V1s #V2s #des #H elim H -V1s -V2s /3 width=1 by lifts_flat/ qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/arith.ma deleted file mode 100644 index 2c47b2873..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/arith.ma +++ /dev/null @@ -1,130 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 "arithmetics/nat.ma". -include "ground_2/star.ma". - -(* ARITHMETICAL PROPERTIES **************************************************) - -(* Equations ****************************************************************) - -lemma plus_n_2: ∀n. n + 2 = n + 1 + 1. -// qed. - -lemma le_plus_minus: ∀m,n,p. p ≤ n → m + n - p = m + (n - p). -/2 by plus_minus/ qed. - -lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → m + n - p = m - p + n. -/2 by plus_minus/ qed. - -lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b. -#a #b #c1 #H >minus_minus_comm >minus_le_minus_minus_comm // -qed. - -lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b. -#a #b #c1 #c2 #H >minus_plus >minus_plus >minus_plus /2 width=1/ -qed. - -lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b. -/3 by monotonic_le_minus_l, le_to_le_to_eq, le_n/ qed. - -lemma arith_h1: ∀a1,a2,b,c1. c1 ≤ a1 → c1 ≤ b → - a1 - c1 + a2 - (b - c1) = a1 + a2 - b. -#a1 #a2 #b #c1 #H1 #H2 >plus_minus // /2 width=1/ -qed. - -(* Inversion & forward lemmas ***********************************************) - -axiom eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2). - -axiom lt_dec: ∀n1,n2. Decidable (n1 < n2). - -lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m. -#m #n elim (lt_or_ge m n) /2 width=1/ -#H elim H -m /2 width=1/ -#m #Hm * #H /2 width=1/ /3 width=1/ -qed-. - -lemma lt_refl_false: ∀n. n < n → ⊥. -#n #H elim (lt_to_not_eq … H) -H /2 width=1/ -qed-. - -lemma lt_zero_false: ∀n. n < 0 → ⊥. -#n #H elim (lt_to_not_le … H) -H /2 width=1/ -qed-. - -lemma false_lt_to_le: ∀x,y. (x < y → ⊥) → y ≤ x. -#x #y #H elim (decidable_lt x y) /2 width=1/ -#Hxy elim (H Hxy) -qed-. - -lemma le_plus_xySz_x_false: ∀y,z,x. x + y + S z ≤ x → ⊥. -#y #z #x elim x -x -[ #H lapply (le_n_O_to_eq … H) -H - commutative_plus // -qed. - -lemma iter_n_Sm: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^l (f b) = f (f^l b). -#B #f #b #l elim l -l normalize // -qed. - -(* Trichotomy operator ******************************************************) - -(* Note: this is "if eqb n1 n2 then a2 else if leb n1 n2 then a1 else a3" *) -let rec tri (A:Type[0]) n1 n2 a1 a2 a3 on n1 : A ≝ - match n1 with - [ O ⇒ match n2 with [ O ⇒ a2 | S n2 ⇒ a1 ] - | S n1 ⇒ match n2 with [ O ⇒ a3 | S n2 ⇒ tri A n1 n2 a1 a2 a3 ] - ]. - -lemma tri_lt: ∀A,a1,a2,a3,n2,n1. n1 < n2 → tri A n1 n2 a1 a2 a3 = a1. -#A #a1 #a2 #a3 #n2 elim n2 -n2 -[ #n1 #H elim (lt_zero_false … H) -| #n2 #IH #n1 elim n1 -n1 // /3 width=1/ -] -qed. - -lemma tri_eq: ∀A,a1,a2,a3,n. tri A n n a1 a2 a3 = a2. -#A #a1 #a2 #a3 #n elim n -n normalize // -qed. - -lemma tri_gt: ∀A,a1,a2,a3,n1,n2. n2 < n1 → tri A n1 n2 a1 a2 a3 = a3. -#A #a1 #a2 #a3 #n1 elim n1 -n1 -[ #n2 #H elim (lt_zero_false … H) -| #n1 #IH #n2 elim n2 -n2 // /3 width=1/ -] -qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma new file mode 100644 index 000000000..7d6f5dda4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma @@ -0,0 +1,130 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "arithmetics/nat.ma". +include "ground_2/lib/star.ma". + +(* ARITHMETICAL PROPERTIES **************************************************) + +(* Equations ****************************************************************) + +lemma plus_n_2: ∀n. n + 2 = n + 1 + 1. +// qed. + +lemma le_plus_minus: ∀m,n,p. p ≤ n → m + n - p = m + (n - p). +/2 by plus_minus/ qed. + +lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → m + n - p = m - p + n. +/2 by plus_minus/ qed. + +lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b. +#a #b #c1 #H >minus_minus_comm >minus_le_minus_minus_comm // +qed. + +lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b. +#a #b #c1 #c2 #H >minus_plus >minus_plus >minus_plus /2 width=1/ +qed. + +lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b. +/3 by monotonic_le_minus_l, le_to_le_to_eq, le_n/ qed. + +lemma arith_h1: ∀a1,a2,b,c1. c1 ≤ a1 → c1 ≤ b → + a1 - c1 + a2 - (b - c1) = a1 + a2 - b. +#a1 #a2 #b #c1 #H1 #H2 >plus_minus // /2 width=1/ +qed. + +(* Inversion & forward lemmas ***********************************************) + +axiom eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2). + +axiom lt_dec: ∀n1,n2. Decidable (n1 < n2). + +lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m. +#m #n elim (lt_or_ge m n) /2 width=1/ +#H elim H -m /2 width=1/ +#m #Hm * #H /2 width=1/ /3 width=1/ +qed-. + +lemma lt_refl_false: ∀n. n < n → ⊥. +#n #H elim (lt_to_not_eq … H) -H /2 width=1/ +qed-. + +lemma lt_zero_false: ∀n. n < 0 → ⊥. +#n #H elim (lt_to_not_le … H) -H /2 width=1/ +qed-. + +lemma false_lt_to_le: ∀x,y. (x < y → ⊥) → y ≤ x. +#x #y #H elim (decidable_lt x y) /2 width=1/ +#Hxy elim (H Hxy) +qed-. + +lemma le_plus_xySz_x_false: ∀y,z,x. x + y + S z ≤ x → ⊥. +#y #z #x elim x -x +[ #H lapply (le_n_O_to_eq … H) -H + commutative_plus // +qed. + +lemma iter_n_Sm: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^l (f b) = f (f^l b). +#B #f #b #l elim l -l normalize // +qed. + +(* Trichotomy operator ******************************************************) + +(* Note: this is "if eqb n1 n2 then a2 else if leb n1 n2 then a1 else a3" *) +let rec tri (A:Type[0]) n1 n2 a1 a2 a3 on n1 : A ≝ + match n1 with + [ O ⇒ match n2 with [ O ⇒ a2 | S n2 ⇒ a1 ] + | S n1 ⇒ match n2 with [ O ⇒ a3 | S n2 ⇒ tri A n1 n2 a1 a2 a3 ] + ]. + +lemma tri_lt: ∀A,a1,a2,a3,n2,n1. n1 < n2 → tri A n1 n2 a1 a2 a3 = a1. +#A #a1 #a2 #a3 #n2 elim n2 -n2 +[ #n1 #H elim (lt_zero_false … H) +| #n2 #IH #n1 elim n1 -n1 // /3 width=1/ +] +qed. + +lemma tri_eq: ∀A,a1,a2,a3,n. tri A n n a1 a2 a3 = a2. +#A #a1 #a2 #a3 #n elim n -n normalize // +qed. + +lemma tri_gt: ∀A,a1,a2,a3,n1,n2. n2 < n1 → tri A n1 n2 a1 a2 a3 = a3. +#A #a1 #a2 #a3 #n1 elim n1 -n1 +[ #n2 #H elim (lt_zero_false … H) +| #n1 #IH #n2 elim n2 -n2 // /3 width=1/ +] +qed. diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma new file mode 100644 index 000000000..d21e1b52b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma @@ -0,0 +1,60 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground_2/notation/constructors/nil_1.ma". +include "ground_2/notation/constructors/nil_2.ma". +include "ground_2/notation/constructors/cons_3.ma". +include "ground_2/notation/constructors/cons_5.ma". +include "ground_2/notation/functions/append_2.ma". +include "ground_2/lib/arith.ma". + +(* LISTS ********************************************************************) + +inductive list (A:Type[0]) : Type[0] := + | nil : list A + | cons: A → list A → list A. + +interpretation "nil (list)" 'Nil A = (nil A). + +interpretation "cons (list)" 'Cons A hd tl = (cons A hd tl). + +let rec all A (R:predicate A) (l:list A) on l ≝ + match l with + [ nil ⇒ ⊤ + | cons hd tl ⇒ R hd ∧ all A R tl + ]. + +inductive list2 (A1,A2:Type[0]) : Type[0] := + | nil2 : list2 A1 A2 + | cons2: A1 → A2 → list2 A1 A2 → list2 A1 A2. + +interpretation "nil (list of pairs)" 'Nil A1 A2 = (nil2 A1 A2). + +interpretation "cons (list of pairs)" 'Cons A1 A2 hd1 hd2 tl = (cons2 A1 A2 hd1 hd2 tl). + +let rec append2 (A1,A2:Type[0]) (l1,l2:list2 A1 A2) on l1 ≝ match l1 with +[ nil2 ⇒ l2 +| cons2 a1 a2 tl ⇒ {a1, a2} @ append2 A1 A2 tl l2 +]. + +interpretation "append (list of pairs)" + 'Append l1 l2 = (append2 ? ? l1 l2). + +let rec length2 (A1,A2:Type[0]) (l:list2 A1 A2) on l ≝ match l with +[ nil2 ⇒ 0 +| cons2 _ _ l ⇒ length2 A1 A2 l + 1 +]. + +interpretation "length (list of pairs)" + 'card l = (length2 ? ? l). diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/lstar.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/lstar.ma new file mode 100644 index 000000000..ae707f2b9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/lstar.ma @@ -0,0 +1,20 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "arithmetics/lstar.ma". + +(* PROPERTIES OF NAT-LABELED REFLEXIVE AND TRANSITIVE CLOSURE ***************) + +definition llstar: ∀A:Type[0]. ∀B. (A→relation B) → nat → (A→relation B) ≝ + λA,B,R,l,a. lstar … (R a) l. diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma new file mode 100644 index 000000000..e5b788766 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/star.ma @@ -0,0 +1,299 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "basics/star1.ma". +include "ground_2/xoa/xoa_props.ma". + +(* PROPERTIES OF RELATIONS **************************************************) + +definition Decidable: Prop → Prop ≝ λR. R ∨ (R → ⊥). + +definition Transitive: ∀A. ∀R: relation A. Prop ≝ λA,R. + ∀a1,a0. R a1 a0 → ∀a2. R a0 a2 → R a1 a2. + +definition confluent2: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2. + ∀a0,a1. R1 a0 a1 → ∀a2. R2 a0 a2 → + ∃∃a. R2 a1 a & R1 a2 a. + +definition transitive2: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2. + ∀a1,a0. R1 a1 a0 → ∀a2. R2 a0 a2 → + ∃∃a. R2 a1 a & R1 a a2. + +definition bi_confluent: ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R. + ∀a0,a1,b0,b1. R a0 b0 a1 b1 → ∀a2,b2. R a0 b0 a2 b2 → + ∃∃a,b. R a1 b1 a b & R a2 b2 a b. + +definition LTC: ∀A:Type[0]. ∀B. (A→relation B) → (A→relation B) ≝ + λA,B,R,a. TC … (R a). + +definition lsub_trans: ∀A,B. relation2 (A→relation B) (relation A) ≝ λA,B,R1,R2. + ∀L2,T1,T2. R1 L2 T1 T2 → ∀L1. R2 L1 L2 → R1 L1 T1 T2. + +definition s_r_trans: ∀A,B. relation2 (A→relation B) (relation A) ≝ λA,B,R1,R2. + ∀L2,T1,T2. R1 L2 T1 T2 → ∀L1. R2 L1 L2 → LTC … R1 L1 T1 T2. + +definition s_rs_trans: ∀A,B. relation2 (A→relation B) (relation A) ≝ λA,B,R1,R2. + ∀L2,T1,T2. LTC … R1 L2 T1 T2 → ∀L1. R2 L1 L2 → LTC … R1 L1 T1 T2. + +lemma TC_strip1: ∀A,R1,R2. confluent2 A R1 R2 → + ∀a0,a1. TC … R1 a0 a1 → ∀a2. R2 a0 a2 → + ∃∃a. R2 a1 a & TC … R1 a2 a. +#A #R1 #R2 #HR12 #a0 #a1 #H elim H -a1 +[ #a1 #Ha01 #a2 #Ha02 + elim (HR12 … Ha01 … Ha02) -HR12 -a0 /3 width=3/ +| #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02 + elim (IHa0 … Ha02) -a0 #a0 #Ha0 #Ha20 + elim (HR12 … Ha1 … Ha0) -HR12 -a /4 width=5/ +] +qed. + +lemma TC_strip2: ∀A,R1,R2. confluent2 A R1 R2 → + ∀a0,a2. TC … R2 a0 a2 → ∀a1. R1 a0 a1 → + ∃∃a. TC … R2 a1 a & R1 a2 a. +#A #R1 #R2 #HR12 #a0 #a2 #H elim H -a2 +[ #a2 #Ha02 #a1 #Ha01 + elim (HR12 … Ha01 … Ha02) -HR12 -a0 /3 width=3/ +| #a #a2 #_ #Ha2 #IHa0 #a1 #Ha01 + elim (IHa0 … Ha01) -a0 #a0 #Ha10 #Ha0 + elim (HR12 … Ha0 … Ha2) -HR12 -a /4 width=3/ +] +qed. + +lemma TC_confluent2: ∀A,R1,R2. + confluent2 A R1 R2 → confluent2 A (TC … R1) (TC … R2). +#A #R1 #R2 #HR12 #a0 #a1 #H elim H -a1 +[ #a1 #Ha01 #a2 #Ha02 + elim (TC_strip2 … HR12 … Ha02 … Ha01) -HR12 -a0 /3 width=3/ +| #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02 + elim (IHa0 … Ha02) -a0 #a0 #Ha0 #Ha20 + elim (TC_strip2 … HR12 … Ha0 … Ha1) -HR12 -a /4 width=5/ +] +qed. + +lemma TC_strap1: ∀A,R1,R2. transitive2 A R1 R2 → + ∀a1,a0. TC … R1 a1 a0 → ∀a2. R2 a0 a2 → + ∃∃a. R2 a1 a & TC … R1 a a2. +#A #R1 #R2 #HR12 #a1 #a0 #H elim H -a0 +[ #a0 #Ha10 #a2 #Ha02 + elim (HR12 … Ha10 … Ha02) -HR12 -a0 /3 width=3/ +| #a #a0 #_ #Ha0 #IHa #a2 #Ha02 + elim (HR12 … Ha0 … Ha02) -HR12 -a0 #a0 #Ha0 #Ha02 + elim (IHa … Ha0) -a /4 width=5/ +] +qed. + +lemma TC_strap2: ∀A,R1,R2. transitive2 A R1 R2 → + ∀a0,a2. TC … R2 a0 a2 → ∀a1. R1 a1 a0 → + ∃∃a. TC … R2 a1 a & R1 a a2. +#A #R1 #R2 #HR12 #a0 #a2 #H elim H -a2 +[ #a2 #Ha02 #a1 #Ha10 + elim (HR12 … Ha10 … Ha02) -HR12 -a0 /3 width=3/ +| #a #a2 #_ #Ha02 #IHa #a1 #Ha10 + elim (IHa … Ha10) -a0 #a0 #Ha10 #Ha0 + elim (HR12 … Ha0 … Ha02) -HR12 -a /4 width=3/ +] +qed. + +lemma TC_transitive2: ∀A,R1,R2. + transitive2 A R1 R2 → transitive2 A (TC … R1) (TC … R2). +#A #R1 #R2 #HR12 #a1 #a0 #H elim H -a0 +[ #a0 #Ha10 #a2 #Ha02 + elim (TC_strap2 … HR12 … Ha02 … Ha10) -HR12 -a0 /3 width=3/ +| #a #a0 #_ #Ha0 #IHa #a2 #Ha02 + elim (TC_strap2 … HR12 … Ha02 … Ha0) -HR12 -a0 #a0 #Ha0 #Ha02 + elim (IHa … Ha0) -a /4 width=5/ +] +qed. + +definition NF: ∀A. relation A → relation A → predicate A ≝ + λA,R,S,a1. ∀a2. R a1 a2 → S a2 a1. + +definition NF_dec: ∀A. relation A → relation A → Prop ≝ + λA,R,S. ∀a1. NF A R S a1 ∨ + ∃∃a2. R … a1 a2 & (S a2 a1 → ⊥). + +inductive SN (A) (R,S:relation A): predicate A ≝ +| SN_intro: ∀a1. (∀a2. R a1 a2 → (S a2 a1 → ⊥) → SN A R S a2) → SN A R S a1 +. + +lemma NF_to_SN: ∀A,R,S,a. NF A R S a → SN A R S a. +#A #R #S #a1 #Ha1 +@SN_intro #a2 #HRa12 #HSa12 +elim HSa12 -HSa12 /2 width=1/ +qed. + +lemma SN_to_NF: ∀A,R,S. NF_dec A R S → + ∀a1. SN A R S a1 → + ∃∃a2. star … R a1 a2 & NF A R S a2. +#A #R #S #HRS #a1 #H elim H -a1 +#a1 #_ #IHa1 elim (HRS a1) -HRS /2 width=3/ +* #a0 #Ha10 #Ha01 elim (IHa1 … Ha10 Ha01) -IHa1 -Ha01 /3 width=3/ +qed-. + +definition NF_sn: ∀A. relation A → relation A → predicate A ≝ + λA,R,S,a2. ∀a1. R a1 a2 → S a2 a1. + +inductive SN_sn (A) (R,S:relation A): predicate A ≝ +| SN_sn_intro: ∀a2. (∀a1. R a1 a2 → (S a2 a1 → ⊥) → SN_sn A R S a1) → SN_sn A R S a2 +. + +lemma NF_to_SN_sn: ∀A,R,S,a. NF_sn A R S a → SN_sn A R S a. +#A #R #S #a2 #Ha2 +@SN_sn_intro #a1 #HRa12 #HSa12 +elim HSa12 -HSa12 /2 width=1/ +qed. + +lemma TC_lsub_trans: ∀A,B,R,S. lsub_trans A B R S → lsub_trans A B (LTC … R) S. +#A #B #R #S #HRS #L2 #T1 #T2 #H elim H -T2 [ /3 width=3/ ] +#T #T2 #_ #HT2 #IHT1 #L1 #HL12 +lapply (HRS … HT2 … HL12) -HRS -HT2 /3 width=3/ +qed-. + +lemma s_r_trans_TC1: ∀A,B,R,S. s_r_trans A B R S → s_rs_trans A B R S. +#A #B #R #S #HRS #L2 #T1 #T2 #H elim H -T2 [ /3 width=3/ ] +#T #T2 #_ #HT2 #IHT1 #L1 #HL12 +lapply (HRS … HT2 … HL12) -HRS -HT2 /3 width=3/ +qed-. + +lemma s_r_trans_TC2: ∀A,B,R,S. s_rs_trans A B R S → s_r_trans A B R (TC … S). +#A #B #R #S #HRS #L2 #T1 #T2 #HT12 #L1 #H @(TC_ind_dx … L1 H) -L1 /2 width=3/ /3 width=3/ +qed-. + +(* relations on unboxed pairs ***********************************************) + +lemma bi_TC_strip: ∀A,B,R. bi_confluent A B R → + ∀a0,a1,b0,b1. R a0 b0 a1 b1 → ∀a2,b2. bi_TC … R a0 b0 a2 b2 → + ∃∃a,b. bi_TC … R a1 b1 a b & R a2 b2 a b. +#A #B #R #HR #a0 #a1 #b0 #b1 #H01 #a2 #b2 #H elim H -a2 -b2 +[ #a2 #b2 #H02 + elim (HR … H01 … H02) -HR -a0 -b0 /3 width=4/ +| #a2 #b2 #a3 #b3 #_ #H23 * #a #b #H1 #H2 + elim (HR … H23 … H2) -HR -a0 -b0 -a2 -b2 /3 width=4/ +] +qed. + +lemma bi_TC_confluent: ∀A,B,R. bi_confluent A B R → + bi_confluent A B (bi_TC … R). +#A #B #R #HR #a0 #a1 #b0 #b1 #H elim H -a1 -b1 +[ #a1 #b1 #H01 #a2 #b2 #H02 + elim (bi_TC_strip … HR … H01 … H02) -a0 -b0 /3 width=4/ +| #a1 #b1 #a3 #b3 #_ #H13 #IH #a2 #b2 #H02 + elim (IH … H02) -a0 -b0 #a0 #b0 #H10 #H20 + elim (bi_TC_strip … HR … H13 … H10) -a1 -b1 /3 width=7/ +] +qed. + +lemma bi_TC_decomp_r: ∀A,B. ∀R:bi_relation A B. + ∀a1,a2,b1,b2. bi_TC … R a1 b1 a2 b2 → + R a1 b1 a2 b2 ∨ + ∃∃a,b. bi_TC … R a1 b1 a b & R a b a2 b2. +#A #B #R #a1 #a2 #b1 #b2 * -a2 -b2 /2 width=1/ /3 width=4/ +qed-. + +lemma bi_TC_decomp_l: ∀A,B. ∀R:bi_relation A B. + ∀a1,a2,b1,b2. bi_TC … R a1 b1 a2 b2 → + R a1 b1 a2 b2 ∨ + ∃∃a,b. R a1 b1 a b & bi_TC … R a b a2 b2. +#A #B #R #a1 #a2 #b1 #b2 #H @(bi_TC_ind_dx … a1 b1 H) -a1 -b1 +[ /2 width=1/ +| #a1 #a #b1 #b #Hab1 #Hab2 #_ /3 width=4/ +] +qed-. + +(* relations on unboxed triples *********************************************) + +definition tri_RC: ∀A,B,C. tri_relation A B C → tri_relation A B C ≝ + λA,B,C,R,a1,b1,c1,a2,b2,c2. R … a1 b1 c1 a2 b2 c2 ∨ + ∧∧ a1 = a2 & b1 = b2 & c1 = c2. + +lemma tri_RC_reflexive: ∀A,B,C,R. tri_reflexive A B C (tri_RC … R). +/3 width=1/ qed. + +definition tri_star: ∀A,B,C,R. tri_relation A B C ≝ + λA,B,C,R. tri_RC A B C (tri_TC … R). + +lemma tri_star_tri_reflexive: ∀A,B,C,R. tri_reflexive A B C (tri_star … R). +/2 width=1/ qed. + +lemma tri_TC_to_tri_star: ∀A,B,C,R,a1,b1,c1,a2,b2,c2. + tri_TC A B C R a1 b1 c1 a2 b2 c2 → + tri_star A B C R a1 b1 c1 a2 b2 c2. +/2 width=1/ qed. + +lemma tri_R_to_tri_star: ∀A,B,C,R,a1,b1,c1,a2,b2,c2. + R a1 b1 c1 a2 b2 c2 → tri_star A B C R a1 b1 c1 a2 b2 c2. +/3 width=1/ qed. + +lemma tri_star_strap1: ∀A,B,C,R,a1,a,a2,b1,b,b2,c1,c,c2. + tri_star A B C R a1 b1 c1 a b c → + R a b c a2 b2 c2 → tri_star A B C R a1 b1 c1 a2 b2 c2. +#A #B #C #R #a1 #a #a2 #b1 #b #b2 #c1 #c #c2 * +[ /3 width=5/ +| * #H1 #H2 #H3 destruct /2 width=1/ +] +qed. + +lemma tri_star_strap2: ∀A,B,C,R,a1,a,a2,b1,b,b2,c1,c,c2. R a1 b1 c1 a b c → + tri_star A B C R a b c a2 b2 c2 → + tri_star A B C R a1 b1 c1 a2 b2 c2. +#A #B #C #R #a1 #a #a2 #b1 #b #b2 #c1 #c #c2 #H * +[ /3 width=5/ +| * #H1 #H2 #H3 destruct /2 width=1/ +] +qed. + +lemma tri_star_to_tri_TC_to_tri_TC: ∀A,B,C,R,a1,a,a2,b1,b,b2,c1,c,c2. + tri_star A B C R a1 b1 c1 a b c → + tri_TC A B C R a b c a2 b2 c2 → + tri_TC A B C R a1 b1 c1 a2 b2 c2. +#A #B #C #R #a1 #a #a2 #b1 #b #b2 #c1 #c #c2 * +[ /2 width=5/ +| * #H1 #H2 #H3 destruct /2 width=1/ +] +qed. + +lemma tri_TC_to_tri_star_to_tri_TC: ∀A,B,C,R,a1,a,a2,b1,b,b2,c1,c,c2. + tri_TC A B C R a1 b1 c1 a b c → + tri_star A B C R a b c a2 b2 c2 → + tri_TC A B C R a1 b1 c1 a2 b2 c2. +#A #B #C #R #a1 #a #a2 #b1 #b #b2 #c1 #c #c2 #H * +[ /2 width=5/ +| * #H1 #H2 #H3 destruct /2 width=1/ +] +qed. + +lemma tri_tansitive_tri_star: ∀A,B,C,R. tri_transitive A B C (tri_star … R). +#A #B #C #R #a1 #a #b1 #b #c1 #c #H #a2 #b2 #c2 * +[ /3 width=5/ +| * #H1 #H2 #H3 destruct /2 width=1/ +] +qed. + +lemma tri_star_ind: ∀A,B,C,R,a1,b1,c1. ∀P:relation3 A B C. P a1 b1 c1 → + (∀a,a2,b,b2,c,c2. tri_star … R a1 b1 c1 a b c → R a b c a2 b2 c2 → P a b c → P a2 b2 c2) → + ∀a2,b2,c2. tri_star … R a1 b1 c1 a2 b2 c2 → P a2 b2 c2. +#A #B #C #R #a1 #b1 #c1 #P #H #IH #a2 #b2 #c2 * +[ #H12 elim H12 -a2 -b2 -c2 /2 width=6/ -H /3 width=6/ +| * #H1 #H2 #H3 destruct // +] +qed-. + +lemma tri_star_ind_dx: ∀A,B,C,R,a2,b2,c2. ∀P:relation3 A B C. P a2 b2 c2 → + (∀a1,a,b1,b,c1,c. R a1 b1 c1 a b c → tri_star … R a b c a2 b2 c2 → P a b c → P a1 b1 c1) → + ∀a1,b1,c1. tri_star … R a1 b1 c1 a2 b2 c2 → P a1 b1 c1. +#A #B #C #R #a2 #b2 #c2 #P #H #IH #a1 #b1 #c1 * +[ #H12 @(tri_TC_ind_dx … a1 b1 c1 H12) -a1 -b1 -c1 /2 width=6/ -H /3 width=6/ +| * #H1 #H2 #H3 destruct // +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/list.ma b/matita/matita/contribs/lambdadelta/ground_2/list.ma deleted file mode 100644 index 9a5ac0aeb..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/list.ma +++ /dev/null @@ -1,55 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 "ground_2/arith.ma". - -(* LISTS ********************************************************************) - -inductive list (A:Type[0]) : Type[0] := - | nil : list A - | cons: A → list A → list A. - -interpretation "nil (list)" 'Nil = (nil ?). - -interpretation "cons (list)" 'Cons hd tl = (cons ? hd tl). - -let rec all A (R:predicate A) (l:list A) on l ≝ - match l with - [ nil ⇒ ⊤ - | cons hd tl ⇒ R hd ∧ all A R tl - ]. - -inductive list2 (A1,A2:Type[0]) : Type[0] := - | nil2 : list2 A1 A2 - | cons2: A1 → A2 → list2 A1 A2 → list2 A1 A2. - -interpretation "nil (list of pairs)" 'Nil2 = (nil2 ? ?). - -interpretation "cons (list of pairs)" 'Cons hd1 hd2 tl = (cons2 ? ? hd1 hd2 tl). - -let rec append2 (A1,A2:Type[0]) (l1,l2:list2 A1 A2) on l1 ≝ match l1 with -[ nil2 ⇒ l2 -| cons2 a1 a2 tl ⇒ {a1, a2} @ append2 A1 A2 tl l2 -]. - -interpretation "append (list of pairs)" - 'Append l1 l2 = (append2 ? ? l1 l2). - -let rec length2 (A1,A2:Type[0]) (l:list2 A1 A2) on l ≝ match l with -[ nil2 ⇒ 0 -| cons2 _ _ l ⇒ length2 A1 A2 l + 1 -]. - -interpretation "length (list of pairs)" - 'card l = (length2 ? ? l). diff --git a/matita/matita/contribs/lambdadelta/ground_2/lstar.ma b/matita/matita/contribs/lambdadelta/ground_2/lstar.ma deleted file mode 100644 index ae707f2b9..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/lstar.ma +++ /dev/null @@ -1,20 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 "arithmetics/lstar.ma". - -(* PROPERTIES OF NAT-LABELED REFLEXIVE AND TRANSITIVE CLOSURE ***************) - -definition llstar: ∀A:Type[0]. ∀B. (A→relation B) → nat → (A→relation B) ≝ - λA,B,R,l,a. lstar … (R a) l. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation.ma b/matita/matita/contribs/lambdadelta/ground_2/notation.ma deleted file mode 100644 index 4ac2e6e64..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/notation.ma +++ /dev/null @@ -1,47 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) - -(* Logic ********************************************************************) - -notation "⊥" - non associative with precedence 90 - for @{'false}. - -notation "⊤" - non associative with precedence 90 - for @{'true}. - -(* Lists ********************************************************************) - -notation "◊" - non associative with precedence 90 - for @{'Nil}. - -notation "hvbox( hd @ break tl )" - right associative with precedence 47 - for @{'Cons $hd $tl}. - -notation "hvbox( l1 @@ break l2 )" - right associative with precedence 47 - for @{'Append $l1 $l2 }. - -notation "⟠" - non associative with precedence 90 - for @{'Nil2}. - -notation "hvbox( { hd1 , break hd2 } @ break tl )" - non associative with precedence 47 - for @{'Cons $hd1 $hd2 $tl}. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_3.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_3.ma new file mode 100644 index 000000000..97fd6e963 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_3.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "hvbox( hd @ break tl )" + right associative with precedence 47 + for @{ 'Cons ? $hd $tl }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_5.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_5.ma new file mode 100644 index 000000000..c8bf11f01 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/cons_5.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "hvbox( { term 46 hd1 , break term 46 hd2 } @ break term 46 tl )" + non associative with precedence 47 + for @{ 'Cons ? ? $hd1 $hd2 $tl }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/nil_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/nil_1.ma new file mode 100644 index 000000000..a6c5e6d54 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/nil_1.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "◊" + non associative with precedence 46 + for @{ 'Nil ? }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/nil_2.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/nil_2.ma new file mode 100644 index 000000000..1a48e23f3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/nil_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "⟠" + non associative with precedence 46 + for @{ 'Nil ? ? }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/functions/append_2.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/append_2.ma new file mode 100644 index 000000000..f6d95184b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/functions/append_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "hvbox( l1 @@ break l2 )" + right associative with precedence 47 + for @{ 'Append $l1 $l2 }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/false_0.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/false_0.ma new file mode 100644 index 000000000..b96432510 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/false_0.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "⊥" + non associative with precedence 19 + for @{'false}. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/true_0.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/true_0.ma new file mode 100644 index 000000000..7a9ad4366 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa/true_0.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "⊤" + non associative with precedence 19 + for @{'true}. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/xoa_notation.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa_notation.ma new file mode 100644 index 000000000..753fc2712 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa_notation.ma @@ -0,0 +1,326 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +(* multiple existental quantifier (1, 2) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.$P0) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) }. + +(* multiple existental quantifier (1, 3) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) }. + +(* multiple existental quantifier (2, 2) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.$P0) (λ${ident x0}.λ${ident x1}.$P1) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) }. + +(* multiple existental quantifier (2, 3) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) }. + +(* multiple existental quantifier (3, 1) *) + +notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.$P0) (λ${ident x0}.$P1) (λ${ident x0}.$P2) }. + +notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) (λ${ident x0}:$T0.$P2) }. + +(* multiple existental quantifier (3, 2) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.$P0) (λ${ident x0}.λ${ident x1}.$P1) (λ${ident x0}.λ${ident x1}.$P2) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P2) }. + +(* multiple existental quantifier (3, 3) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) }. + +(* multiple existental quantifier (3, 4) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) }. + +(* multiple existental quantifier (4, 1) *) + +notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.$P0) (λ${ident x0}.$P1) (λ${ident x0}.$P2) (λ${ident x0}.$P3) }. + +notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) (λ${ident x0}:$T0.$P2) (λ${ident x0}:$T0.$P3) }. + +(* multiple existental quantifier (4, 2) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.$P0) (λ${ident x0}.λ${ident x1}.$P1) (λ${ident x0}.λ${ident x1}.$P2) (λ${ident x0}.λ${ident x1}.$P3) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P3) }. + +(* multiple existental quantifier (4, 3) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P3) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) }. + +(* multiple existental quantifier (4, 4) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P3) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) }. + +(* multiple existental quantifier (4, 5) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P3) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) }. + +(* multiple existental quantifier (5, 2) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.$P0) (λ${ident x0}.λ${ident x1}.$P1) (λ${ident x0}.λ${ident x1}.$P2) (λ${ident x0}.λ${ident x1}.$P3) (λ${ident x0}.λ${ident x1}.$P4) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P4) }. + +(* multiple existental quantifier (5, 3) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P4) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P4) }. + +(* multiple existental quantifier (5, 4) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P4) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) }. + +(* multiple existental quantifier (5, 5) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P4) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P4) }. + +(* multiple existental quantifier (5, 6) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P4) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P4) }. + +(* multiple existental quantifier (6, 3) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P5) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P5) }. + +(* multiple existental quantifier (6, 4) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P5) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P5) }. + +(* multiple existental quantifier (6, 5) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P5) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P5) }. + +(* multiple existental quantifier (6, 6) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P5) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P5) }. + +(* multiple existental quantifier (6, 7) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P5) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P5) }. + +(* multiple existental quantifier (7, 4) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P6) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P6) }. + +(* multiple existental quantifier (7, 7) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P6) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P6) }. + +(* multiple existental quantifier (8, 5) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P6) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P7) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P6) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P7) }. + +(* multiple existental quantifier (9, 3) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7 break & term 19 P8)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P6) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P7) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P8) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7 break & term 19 P8)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P6) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P7) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P8) }. + +(* multiple existental quantifier (10, 4) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7 break & term 19 P8 break & term 19 P9)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P6) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P7) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P8) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P9) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7 break & term 19 P8 break & term 19 P9)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P6) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P7) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P8) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P9) }. + +(* multiple disjunction connective (3) *) + +notation "hvbox(∨∨ term 29 P0 break | term 29 P1 break | term 29 P2)" + non associative with precedence 30 + for @{ 'Or $P0 $P1 $P2 }. + +(* multiple disjunction connective (4) *) + +notation "hvbox(∨∨ term 29 P0 break | term 29 P1 break | term 29 P2 break | term 29 P3)" + non associative with precedence 30 + for @{ 'Or $P0 $P1 $P2 $P3 }. + +(* multiple disjunction connective (5) *) + +notation "hvbox(∨∨ term 29 P0 break | term 29 P1 break | term 29 P2 break | term 29 P3 break | term 29 P4)" + non associative with precedence 30 + for @{ 'Or $P0 $P1 $P2 $P3 $P4 }. + +(* multiple conjunction connective (3) *) + +notation "hvbox(∧∧ term 34 P0 break & term 34 P1 break & term 34 P2)" + non associative with precedence 35 + for @{ 'And $P0 $P1 $P2 }. + +(* multiple conjunction connective (4) *) + +notation "hvbox(∧∧ term 34 P0 break & term 34 P1 break & term 34 P2 break & term 34 P3)" + non associative with precedence 35 + for @{ 'And $P0 $P1 $P2 $P3 }. + diff --git a/matita/matita/contribs/lambdadelta/ground_2/star.ma b/matita/matita/contribs/lambdadelta/ground_2/star.ma deleted file mode 100644 index 29131d108..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/star.ma +++ /dev/null @@ -1,300 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 "basics/star1.ma". -include "ground_2/xoa_props.ma". -include "ground_2/notation.ma". - -(* PROPERTIES OF RELATIONS **************************************************) - -definition Decidable: Prop → Prop ≝ λR. R ∨ (R → ⊥). - -definition Transitive: ∀A. ∀R: relation A. Prop ≝ λA,R. - ∀a1,a0. R a1 a0 → ∀a2. R a0 a2 → R a1 a2. - -definition confluent2: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2. - ∀a0,a1. R1 a0 a1 → ∀a2. R2 a0 a2 → - ∃∃a. R2 a1 a & R1 a2 a. - -definition transitive2: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2. - ∀a1,a0. R1 a1 a0 → ∀a2. R2 a0 a2 → - ∃∃a. R2 a1 a & R1 a a2. - -definition bi_confluent: ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R. - ∀a0,a1,b0,b1. R a0 b0 a1 b1 → ∀a2,b2. R a0 b0 a2 b2 → - ∃∃a,b. R a1 b1 a b & R a2 b2 a b. - -definition LTC: ∀A:Type[0]. ∀B. (A→relation B) → (A→relation B) ≝ - λA,B,R,a. TC … (R a). - -definition lsub_trans: ∀A,B. relation2 (A→relation B) (relation A) ≝ λA,B,R1,R2. - ∀L2,T1,T2. R1 L2 T1 T2 → ∀L1. R2 L1 L2 → R1 L1 T1 T2. - -definition s_r_trans: ∀A,B. relation2 (A→relation B) (relation A) ≝ λA,B,R1,R2. - ∀L2,T1,T2. R1 L2 T1 T2 → ∀L1. R2 L1 L2 → LTC … R1 L1 T1 T2. - -definition s_rs_trans: ∀A,B. relation2 (A→relation B) (relation A) ≝ λA,B,R1,R2. - ∀L2,T1,T2. LTC … R1 L2 T1 T2 → ∀L1. R2 L1 L2 → LTC … R1 L1 T1 T2. - -lemma TC_strip1: ∀A,R1,R2. confluent2 A R1 R2 → - ∀a0,a1. TC … R1 a0 a1 → ∀a2. R2 a0 a2 → - ∃∃a. R2 a1 a & TC … R1 a2 a. -#A #R1 #R2 #HR12 #a0 #a1 #H elim H -a1 -[ #a1 #Ha01 #a2 #Ha02 - elim (HR12 … Ha01 … Ha02) -HR12 -a0 /3 width=3/ -| #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02 - elim (IHa0 … Ha02) -a0 #a0 #Ha0 #Ha20 - elim (HR12 … Ha1 … Ha0) -HR12 -a /4 width=5/ -] -qed. - -lemma TC_strip2: ∀A,R1,R2. confluent2 A R1 R2 → - ∀a0,a2. TC … R2 a0 a2 → ∀a1. R1 a0 a1 → - ∃∃a. TC … R2 a1 a & R1 a2 a. -#A #R1 #R2 #HR12 #a0 #a2 #H elim H -a2 -[ #a2 #Ha02 #a1 #Ha01 - elim (HR12 … Ha01 … Ha02) -HR12 -a0 /3 width=3/ -| #a #a2 #_ #Ha2 #IHa0 #a1 #Ha01 - elim (IHa0 … Ha01) -a0 #a0 #Ha10 #Ha0 - elim (HR12 … Ha0 … Ha2) -HR12 -a /4 width=3/ -] -qed. - -lemma TC_confluent2: ∀A,R1,R2. - confluent2 A R1 R2 → confluent2 A (TC … R1) (TC … R2). -#A #R1 #R2 #HR12 #a0 #a1 #H elim H -a1 -[ #a1 #Ha01 #a2 #Ha02 - elim (TC_strip2 … HR12 … Ha02 … Ha01) -HR12 -a0 /3 width=3/ -| #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02 - elim (IHa0 … Ha02) -a0 #a0 #Ha0 #Ha20 - elim (TC_strip2 … HR12 … Ha0 … Ha1) -HR12 -a /4 width=5/ -] -qed. - -lemma TC_strap1: ∀A,R1,R2. transitive2 A R1 R2 → - ∀a1,a0. TC … R1 a1 a0 → ∀a2. R2 a0 a2 → - ∃∃a. R2 a1 a & TC … R1 a a2. -#A #R1 #R2 #HR12 #a1 #a0 #H elim H -a0 -[ #a0 #Ha10 #a2 #Ha02 - elim (HR12 … Ha10 … Ha02) -HR12 -a0 /3 width=3/ -| #a #a0 #_ #Ha0 #IHa #a2 #Ha02 - elim (HR12 … Ha0 … Ha02) -HR12 -a0 #a0 #Ha0 #Ha02 - elim (IHa … Ha0) -a /4 width=5/ -] -qed. - -lemma TC_strap2: ∀A,R1,R2. transitive2 A R1 R2 → - ∀a0,a2. TC … R2 a0 a2 → ∀a1. R1 a1 a0 → - ∃∃a. TC … R2 a1 a & R1 a a2. -#A #R1 #R2 #HR12 #a0 #a2 #H elim H -a2 -[ #a2 #Ha02 #a1 #Ha10 - elim (HR12 … Ha10 … Ha02) -HR12 -a0 /3 width=3/ -| #a #a2 #_ #Ha02 #IHa #a1 #Ha10 - elim (IHa … Ha10) -a0 #a0 #Ha10 #Ha0 - elim (HR12 … Ha0 … Ha02) -HR12 -a /4 width=3/ -] -qed. - -lemma TC_transitive2: ∀A,R1,R2. - transitive2 A R1 R2 → transitive2 A (TC … R1) (TC … R2). -#A #R1 #R2 #HR12 #a1 #a0 #H elim H -a0 -[ #a0 #Ha10 #a2 #Ha02 - elim (TC_strap2 … HR12 … Ha02 … Ha10) -HR12 -a0 /3 width=3/ -| #a #a0 #_ #Ha0 #IHa #a2 #Ha02 - elim (TC_strap2 … HR12 … Ha02 … Ha0) -HR12 -a0 #a0 #Ha0 #Ha02 - elim (IHa … Ha0) -a /4 width=5/ -] -qed. - -definition NF: ∀A. relation A → relation A → predicate A ≝ - λA,R,S,a1. ∀a2. R a1 a2 → S a2 a1. - -definition NF_dec: ∀A. relation A → relation A → Prop ≝ - λA,R,S. ∀a1. NF A R S a1 ∨ - ∃∃a2. R … a1 a2 & (S a2 a1 → ⊥). - -inductive SN (A) (R,S:relation A): predicate A ≝ -| SN_intro: ∀a1. (∀a2. R a1 a2 → (S a2 a1 → ⊥) → SN A R S a2) → SN A R S a1 -. - -lemma NF_to_SN: ∀A,R,S,a. NF A R S a → SN A R S a. -#A #R #S #a1 #Ha1 -@SN_intro #a2 #HRa12 #HSa12 -elim HSa12 -HSa12 /2 width=1/ -qed. - -lemma SN_to_NF: ∀A,R,S. NF_dec A R S → - ∀a1. SN A R S a1 → - ∃∃a2. star … R a1 a2 & NF A R S a2. -#A #R #S #HRS #a1 #H elim H -a1 -#a1 #_ #IHa1 elim (HRS a1) -HRS /2 width=3/ -* #a0 #Ha10 #Ha01 elim (IHa1 … Ha10 Ha01) -IHa1 -Ha01 /3 width=3/ -qed-. - -definition NF_sn: ∀A. relation A → relation A → predicate A ≝ - λA,R,S,a2. ∀a1. R a1 a2 → S a2 a1. - -inductive SN_sn (A) (R,S:relation A): predicate A ≝ -| SN_sn_intro: ∀a2. (∀a1. R a1 a2 → (S a2 a1 → ⊥) → SN_sn A R S a1) → SN_sn A R S a2 -. - -lemma NF_to_SN_sn: ∀A,R,S,a. NF_sn A R S a → SN_sn A R S a. -#A #R #S #a2 #Ha2 -@SN_sn_intro #a1 #HRa12 #HSa12 -elim HSa12 -HSa12 /2 width=1/ -qed. - -lemma TC_lsub_trans: ∀A,B,R,S. lsub_trans A B R S → lsub_trans A B (LTC … R) S. -#A #B #R #S #HRS #L2 #T1 #T2 #H elim H -T2 [ /3 width=3/ ] -#T #T2 #_ #HT2 #IHT1 #L1 #HL12 -lapply (HRS … HT2 … HL12) -HRS -HT2 /3 width=3/ -qed-. - -lemma s_r_trans_TC1: ∀A,B,R,S. s_r_trans A B R S → s_rs_trans A B R S. -#A #B #R #S #HRS #L2 #T1 #T2 #H elim H -T2 [ /3 width=3/ ] -#T #T2 #_ #HT2 #IHT1 #L1 #HL12 -lapply (HRS … HT2 … HL12) -HRS -HT2 /3 width=3/ -qed-. - -lemma s_r_trans_TC2: ∀A,B,R,S. s_rs_trans A B R S → s_r_trans A B R (TC … S). -#A #B #R #S #HRS #L2 #T1 #T2 #HT12 #L1 #H @(TC_ind_dx … L1 H) -L1 /2 width=3/ /3 width=3/ -qed-. - -(* relations on unboxed pairs ***********************************************) - -lemma bi_TC_strip: ∀A,B,R. bi_confluent A B R → - ∀a0,a1,b0,b1. R a0 b0 a1 b1 → ∀a2,b2. bi_TC … R a0 b0 a2 b2 → - ∃∃a,b. bi_TC … R a1 b1 a b & R a2 b2 a b. -#A #B #R #HR #a0 #a1 #b0 #b1 #H01 #a2 #b2 #H elim H -a2 -b2 -[ #a2 #b2 #H02 - elim (HR … H01 … H02) -HR -a0 -b0 /3 width=4/ -| #a2 #b2 #a3 #b3 #_ #H23 * #a #b #H1 #H2 - elim (HR … H23 … H2) -HR -a0 -b0 -a2 -b2 /3 width=4/ -] -qed. - -lemma bi_TC_confluent: ∀A,B,R. bi_confluent A B R → - bi_confluent A B (bi_TC … R). -#A #B #R #HR #a0 #a1 #b0 #b1 #H elim H -a1 -b1 -[ #a1 #b1 #H01 #a2 #b2 #H02 - elim (bi_TC_strip … HR … H01 … H02) -a0 -b0 /3 width=4/ -| #a1 #b1 #a3 #b3 #_ #H13 #IH #a2 #b2 #H02 - elim (IH … H02) -a0 -b0 #a0 #b0 #H10 #H20 - elim (bi_TC_strip … HR … H13 … H10) -a1 -b1 /3 width=7/ -] -qed. - -lemma bi_TC_decomp_r: ∀A,B. ∀R:bi_relation A B. - ∀a1,a2,b1,b2. bi_TC … R a1 b1 a2 b2 → - R a1 b1 a2 b2 ∨ - ∃∃a,b. bi_TC … R a1 b1 a b & R a b a2 b2. -#A #B #R #a1 #a2 #b1 #b2 * -a2 -b2 /2 width=1/ /3 width=4/ -qed-. - -lemma bi_TC_decomp_l: ∀A,B. ∀R:bi_relation A B. - ∀a1,a2,b1,b2. bi_TC … R a1 b1 a2 b2 → - R a1 b1 a2 b2 ∨ - ∃∃a,b. R a1 b1 a b & bi_TC … R a b a2 b2. -#A #B #R #a1 #a2 #b1 #b2 #H @(bi_TC_ind_dx … a1 b1 H) -a1 -b1 -[ /2 width=1/ -| #a1 #a #b1 #b #Hab1 #Hab2 #_ /3 width=4/ -] -qed-. - -(* relations on unboxed triples *********************************************) - -definition tri_RC: ∀A,B,C. tri_relation A B C → tri_relation A B C ≝ - λA,B,C,R,a1,b1,c1,a2,b2,c2. R … a1 b1 c1 a2 b2 c2 ∨ - ∧∧ a1 = a2 & b1 = b2 & c1 = c2. - -lemma tri_RC_reflexive: ∀A,B,C,R. tri_reflexive A B C (tri_RC … R). -/3 width=1/ qed. - -definition tri_star: ∀A,B,C,R. tri_relation A B C ≝ - λA,B,C,R. tri_RC A B C (tri_TC … R). - -lemma tri_star_tri_reflexive: ∀A,B,C,R. tri_reflexive A B C (tri_star … R). -/2 width=1/ qed. - -lemma tri_TC_to_tri_star: ∀A,B,C,R,a1,b1,c1,a2,b2,c2. - tri_TC A B C R a1 b1 c1 a2 b2 c2 → - tri_star A B C R a1 b1 c1 a2 b2 c2. -/2 width=1/ qed. - -lemma tri_R_to_tri_star: ∀A,B,C,R,a1,b1,c1,a2,b2,c2. - R a1 b1 c1 a2 b2 c2 → tri_star A B C R a1 b1 c1 a2 b2 c2. -/3 width=1/ qed. - -lemma tri_star_strap1: ∀A,B,C,R,a1,a,a2,b1,b,b2,c1,c,c2. - tri_star A B C R a1 b1 c1 a b c → - R a b c a2 b2 c2 → tri_star A B C R a1 b1 c1 a2 b2 c2. -#A #B #C #R #a1 #a #a2 #b1 #b #b2 #c1 #c #c2 * -[ /3 width=5/ -| * #H1 #H2 #H3 destruct /2 width=1/ -] -qed. - -lemma tri_star_strap2: ∀A,B,C,R,a1,a,a2,b1,b,b2,c1,c,c2. R a1 b1 c1 a b c → - tri_star A B C R a b c a2 b2 c2 → - tri_star A B C R a1 b1 c1 a2 b2 c2. -#A #B #C #R #a1 #a #a2 #b1 #b #b2 #c1 #c #c2 #H * -[ /3 width=5/ -| * #H1 #H2 #H3 destruct /2 width=1/ -] -qed. - -lemma tri_star_to_tri_TC_to_tri_TC: ∀A,B,C,R,a1,a,a2,b1,b,b2,c1,c,c2. - tri_star A B C R a1 b1 c1 a b c → - tri_TC A B C R a b c a2 b2 c2 → - tri_TC A B C R a1 b1 c1 a2 b2 c2. -#A #B #C #R #a1 #a #a2 #b1 #b #b2 #c1 #c #c2 * -[ /2 width=5/ -| * #H1 #H2 #H3 destruct /2 width=1/ -] -qed. - -lemma tri_TC_to_tri_star_to_tri_TC: ∀A,B,C,R,a1,a,a2,b1,b,b2,c1,c,c2. - tri_TC A B C R a1 b1 c1 a b c → - tri_star A B C R a b c a2 b2 c2 → - tri_TC A B C R a1 b1 c1 a2 b2 c2. -#A #B #C #R #a1 #a #a2 #b1 #b #b2 #c1 #c #c2 #H * -[ /2 width=5/ -| * #H1 #H2 #H3 destruct /2 width=1/ -] -qed. - -lemma tri_tansitive_tri_star: ∀A,B,C,R. tri_transitive A B C (tri_star … R). -#A #B #C #R #a1 #a #b1 #b #c1 #c #H #a2 #b2 #c2 * -[ /3 width=5/ -| * #H1 #H2 #H3 destruct /2 width=1/ -] -qed. - -lemma tri_star_ind: ∀A,B,C,R,a1,b1,c1. ∀P:relation3 A B C. P a1 b1 c1 → - (∀a,a2,b,b2,c,c2. tri_star … R a1 b1 c1 a b c → R a b c a2 b2 c2 → P a b c → P a2 b2 c2) → - ∀a2,b2,c2. tri_star … R a1 b1 c1 a2 b2 c2 → P a2 b2 c2. -#A #B #C #R #a1 #b1 #c1 #P #H #IH #a2 #b2 #c2 * -[ #H12 elim H12 -a2 -b2 -c2 /2 width=6/ -H /3 width=6/ -| * #H1 #H2 #H3 destruct // -] -qed-. - -lemma tri_star_ind_dx: ∀A,B,C,R,a2,b2,c2. ∀P:relation3 A B C. P a2 b2 c2 → - (∀a1,a,b1,b,c1,c. R a1 b1 c1 a b c → tri_star … R a b c a2 b2 c2 → P a b c → P a1 b1 c1) → - ∀a1,b1,c1. tri_star … R a1 b1 c1 a2 b2 c2 → P a1 b1 c1. -#A #B #C #R #a2 #b2 #c2 #P #H #IH #a1 #b1 #c1 * -[ #H12 @(tri_TC_ind_dx … a1 b1 c1 H12) -a1 -b1 -c1 /2 width=6/ -H /3 width=6/ -| * #H1 #H2 #H3 destruct // -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml b/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml index 79cd48b52..43d1b9366 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml @@ -1,9 +1,9 @@
- contribs/lambdadelta/ground_2/ - xoa - xoa_notation + contribs/lambdadelta/ + ground_2/xoa/xoa + ground_2/notation/xoa_notation basics/pts.ma 1 2 1 3 diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa.ma deleted file mode 100644 index 625be0c7f..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa.ma +++ /dev/null @@ -1,291 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -(* This file was generated by xoa.native: do not edit *********************) - -include "basics/pts.ma". - -(* multiple existental quantifier (1, 2) *) - -inductive ex1_2 (A0,A1:Type[0]) (P0:A0→A1→Prop) : Prop ≝ - | ex1_2_intro: ∀x0,x1. P0 x0 x1 → ex1_2 ? ? ? -. - -interpretation "multiple existental quantifier (1, 2)" 'Ex P0 = (ex1_2 ? ? P0). - -(* multiple existental quantifier (1, 3) *) - -inductive ex1_3 (A0,A1,A2:Type[0]) (P0:A0→A1→A2→Prop) : Prop ≝ - | ex1_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → ex1_3 ? ? ? ? -. - -interpretation "multiple existental quantifier (1, 3)" 'Ex P0 = (ex1_3 ? ? ? P0). - -(* multiple existental quantifier (2, 2) *) - -inductive ex2_2 (A0,A1:Type[0]) (P0,P1:A0→A1→Prop) : Prop ≝ - | ex2_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → ex2_2 ? ? ? ? -. - -interpretation "multiple existental quantifier (2, 2)" 'Ex P0 P1 = (ex2_2 ? ? P0 P1). - -(* multiple existental quantifier (2, 3) *) - -inductive ex2_3 (A0,A1,A2:Type[0]) (P0,P1:A0→A1→A2→Prop) : Prop ≝ - | ex2_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → ex2_3 ? ? ? ? ? -. - -interpretation "multiple existental quantifier (2, 3)" 'Ex P0 P1 = (ex2_3 ? ? ? P0 P1). - -(* multiple existental quantifier (3, 1) *) - -inductive ex3 (A0:Type[0]) (P0,P1,P2:A0→Prop) : Prop ≝ - | ex3_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → ex3 ? ? ? ? -. - -interpretation "multiple existental quantifier (3, 1)" 'Ex P0 P1 P2 = (ex3 ? P0 P1 P2). - -(* multiple existental quantifier (3, 2) *) - -inductive ex3_2 (A0,A1:Type[0]) (P0,P1,P2:A0→A1→Prop) : Prop ≝ - | ex3_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → P2 x0 x1 → ex3_2 ? ? ? ? ? -. - -interpretation "multiple existental quantifier (3, 2)" 'Ex P0 P1 P2 = (ex3_2 ? ? P0 P1 P2). - -(* multiple existental quantifier (3, 3) *) - -inductive ex3_3 (A0,A1,A2:Type[0]) (P0,P1,P2:A0→A1→A2→Prop) : Prop ≝ - | ex3_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → ex3_3 ? ? ? ? ? ? -. - -interpretation "multiple existental quantifier (3, 3)" 'Ex P0 P1 P2 = (ex3_3 ? ? ? P0 P1 P2). - -(* multiple existental quantifier (3, 4) *) - -inductive ex3_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2:A0→A1→A2→A3→Prop) : Prop ≝ - | ex3_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → ex3_4 ? ? ? ? ? ? ? -. - -interpretation "multiple existental quantifier (3, 4)" 'Ex P0 P1 P2 = (ex3_4 ? ? ? ? P0 P1 P2). - -(* multiple existental quantifier (4, 1) *) - -inductive ex4 (A0:Type[0]) (P0,P1,P2,P3:A0→Prop) : Prop ≝ - | ex4_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → P3 x0 → ex4 ? ? ? ? ? -. - -interpretation "multiple existental quantifier (4, 1)" 'Ex P0 P1 P2 P3 = (ex4 ? P0 P1 P2 P3). - -(* multiple existental quantifier (4, 2) *) - -inductive ex4_2 (A0,A1:Type[0]) (P0,P1,P2,P3:A0→A1→Prop) : Prop ≝ - | ex4_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → P2 x0 x1 → P3 x0 x1 → ex4_2 ? ? ? ? ? ? -. - -interpretation "multiple existental quantifier (4, 2)" 'Ex P0 P1 P2 P3 = (ex4_2 ? ? P0 P1 P2 P3). - -(* multiple existental quantifier (4, 3) *) - -inductive ex4_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3:A0→A1→A2→Prop) : Prop ≝ - | ex4_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → ex4_3 ? ? ? ? ? ? ? -. - -interpretation "multiple existental quantifier (4, 3)" 'Ex P0 P1 P2 P3 = (ex4_3 ? ? ? P0 P1 P2 P3). - -(* multiple existental quantifier (4, 4) *) - -inductive ex4_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3:A0→A1→A2→A3→Prop) : Prop ≝ - | ex4_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → ex4_4 ? ? ? ? ? ? ? ? -. - -interpretation "multiple existental quantifier (4, 4)" 'Ex P0 P1 P2 P3 = (ex4_4 ? ? ? ? P0 P1 P2 P3). - -(* multiple existental quantifier (4, 5) *) - -inductive ex4_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3:A0→A1→A2→A3→A4→Prop) : Prop ≝ - | ex4_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → ex4_5 ? ? ? ? ? ? ? ? ? -. - -interpretation "multiple existental quantifier (4, 5)" 'Ex P0 P1 P2 P3 = (ex4_5 ? ? ? ? ? P0 P1 P2 P3). - -(* multiple existental quantifier (5, 2) *) - -inductive ex5_2 (A0,A1:Type[0]) (P0,P1,P2,P3,P4:A0→A1→Prop) : Prop ≝ - | ex5_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → P2 x0 x1 → P3 x0 x1 → P4 x0 x1 → ex5_2 ? ? ? ? ? ? ? -. - -interpretation "multiple existental quantifier (5, 2)" 'Ex P0 P1 P2 P3 P4 = (ex5_2 ? ? P0 P1 P2 P3 P4). - -(* multiple existental quantifier (5, 3) *) - -inductive ex5_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→Prop) : Prop ≝ - | ex5_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → P4 x0 x1 x2 → ex5_3 ? ? ? ? ? ? ? ? -. - -interpretation "multiple existental quantifier (5, 3)" 'Ex P0 P1 P2 P3 P4 = (ex5_3 ? ? ? P0 P1 P2 P3 P4). - -(* multiple existental quantifier (5, 4) *) - -inductive ex5_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→A3→Prop) : Prop ≝ - | ex5_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → ex5_4 ? ? ? ? ? ? ? ? ? -. - -interpretation "multiple existental quantifier (5, 4)" 'Ex P0 P1 P2 P3 P4 = (ex5_4 ? ? ? ? P0 P1 P2 P3 P4). - -(* multiple existental quantifier (5, 5) *) - -inductive ex5_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→A3→A4→Prop) : Prop ≝ - | ex5_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → P4 x0 x1 x2 x3 x4 → ex5_5 ? ? ? ? ? ? ? ? ? ? -. - -interpretation "multiple existental quantifier (5, 5)" 'Ex P0 P1 P2 P3 P4 = (ex5_5 ? ? ? ? ? P0 P1 P2 P3 P4). - -(* multiple existental quantifier (5, 6) *) - -inductive ex5_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→A3→A4→A5→Prop) : Prop ≝ - | ex5_6_intro: ∀x0,x1,x2,x3,x4,x5. P0 x0 x1 x2 x3 x4 x5 → P1 x0 x1 x2 x3 x4 x5 → P2 x0 x1 x2 x3 x4 x5 → P3 x0 x1 x2 x3 x4 x5 → P4 x0 x1 x2 x3 x4 x5 → ex5_6 ? ? ? ? ? ? ? ? ? ? ? -. - -interpretation "multiple existental quantifier (5, 6)" 'Ex P0 P1 P2 P3 P4 = (ex5_6 ? ? ? ? ? ? P0 P1 P2 P3 P4). - -(* multiple existental quantifier (6, 3) *) - -inductive ex6_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→Prop) : Prop ≝ - | ex6_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → P4 x0 x1 x2 → P5 x0 x1 x2 → ex6_3 ? ? ? ? ? ? ? ? ? -. - -interpretation "multiple existental quantifier (6, 3)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_3 ? ? ? P0 P1 P2 P3 P4 P5). - -(* multiple existental quantifier (6, 4) *) - -inductive ex6_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→Prop) : Prop ≝ - | ex6_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → P5 x0 x1 x2 x3 → ex6_4 ? ? ? ? ? ? ? ? ? ? -. - -interpretation "multiple existental quantifier (6, 4)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_4 ? ? ? ? P0 P1 P2 P3 P4 P5). - -(* multiple existental quantifier (6, 5) *) - -inductive ex6_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→A4→Prop) : Prop ≝ - | ex6_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → P4 x0 x1 x2 x3 x4 → P5 x0 x1 x2 x3 x4 → ex6_5 ? ? ? ? ? ? ? ? ? ? ? -. - -interpretation "multiple existental quantifier (6, 5)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_5 ? ? ? ? ? P0 P1 P2 P3 P4 P5). - -(* multiple existental quantifier (6, 6) *) - -inductive ex6_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→A4→A5→Prop) : Prop ≝ - | ex6_6_intro: ∀x0,x1,x2,x3,x4,x5. P0 x0 x1 x2 x3 x4 x5 → P1 x0 x1 x2 x3 x4 x5 → P2 x0 x1 x2 x3 x4 x5 → P3 x0 x1 x2 x3 x4 x5 → P4 x0 x1 x2 x3 x4 x5 → P5 x0 x1 x2 x3 x4 x5 → ex6_6 ? ? ? ? ? ? ? ? ? ? ? ? -. - -interpretation "multiple existental quantifier (6, 6)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_6 ? ? ? ? ? ? P0 P1 P2 P3 P4 P5). - -(* multiple existental quantifier (6, 7) *) - -inductive ex6_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→A4→A5→A6→Prop) : Prop ≝ - | ex6_7_intro: ∀x0,x1,x2,x3,x4,x5,x6. P0 x0 x1 x2 x3 x4 x5 x6 → P1 x0 x1 x2 x3 x4 x5 x6 → P2 x0 x1 x2 x3 x4 x5 x6 → P3 x0 x1 x2 x3 x4 x5 x6 → P4 x0 x1 x2 x3 x4 x5 x6 → P5 x0 x1 x2 x3 x4 x5 x6 → ex6_7 ? ? ? ? ? ? ? ? ? ? ? ? ? -. - -interpretation "multiple existental quantifier (6, 7)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5). - -(* multiple existental quantifier (7, 4) *) - -inductive ex7_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→Prop) : Prop ≝ - | ex7_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → P5 x0 x1 x2 x3 → P6 x0 x1 x2 x3 → ex7_4 ? ? ? ? ? ? ? ? ? ? ? -. - -interpretation "multiple existental quantifier (7, 4)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6). - -(* multiple existental quantifier (7, 7) *) - -inductive ex7_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→A5→A6→Prop) : Prop ≝ - | ex7_7_intro: ∀x0,x1,x2,x3,x4,x5,x6. P0 x0 x1 x2 x3 x4 x5 x6 → P1 x0 x1 x2 x3 x4 x5 x6 → P2 x0 x1 x2 x3 x4 x5 x6 → P3 x0 x1 x2 x3 x4 x5 x6 → P4 x0 x1 x2 x3 x4 x5 x6 → P5 x0 x1 x2 x3 x4 x5 x6 → P6 x0 x1 x2 x3 x4 x5 x6 → ex7_7 ? ? ? ? ? ? ? ? ? ? ? ? ? ? -. - -interpretation "multiple existental quantifier (7, 7)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6). - -(* multiple existental quantifier (8, 5) *) - -inductive ex8_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3,P4,P5,P6,P7:A0→A1→A2→A3→A4→Prop) : Prop ≝ - | ex8_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → P4 x0 x1 x2 x3 x4 → P5 x0 x1 x2 x3 x4 → P6 x0 x1 x2 x3 x4 → P7 x0 x1 x2 x3 x4 → ex8_5 ? ? ? ? ? ? ? ? ? ? ? ? ? -. - -interpretation "multiple existental quantifier (8, 5)" 'Ex P0 P1 P2 P3 P4 P5 P6 P7 = (ex8_5 ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6 P7). - -(* multiple existental quantifier (9, 3) *) - -inductive ex9_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4,P5,P6,P7,P8:A0→A1→A2→Prop) : Prop ≝ - | ex9_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → P4 x0 x1 x2 → P5 x0 x1 x2 → P6 x0 x1 x2 → P7 x0 x1 x2 → P8 x0 x1 x2 → ex9_3 ? ? ? ? ? ? ? ? ? ? ? ? -. - -interpretation "multiple existental quantifier (9, 3)" 'Ex P0 P1 P2 P3 P4 P5 P6 P7 P8 = (ex9_3 ? ? ? P0 P1 P2 P3 P4 P5 P6 P7 P8). - -(* multiple existental quantifier (10, 4) *) - -inductive ex10_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5,P6,P7,P8,P9:A0→A1→A2→A3→Prop) : Prop ≝ - | ex10_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → P5 x0 x1 x2 x3 → P6 x0 x1 x2 x3 → P7 x0 x1 x2 x3 → P8 x0 x1 x2 x3 → P9 x0 x1 x2 x3 → ex10_4 ? ? ? ? ? ? ? ? ? ? ? ? ? ? -. - -interpretation "multiple existental quantifier (10, 4)" 'Ex P0 P1 P2 P3 P4 P5 P6 P7 P8 P9 = (ex10_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6 P7 P8 P9). - -(* multiple disjunction connective (3) *) - -inductive or3 (P0,P1,P2:Prop) : Prop ≝ - | or3_intro0: P0 → or3 ? ? ? - | or3_intro1: P1 → or3 ? ? ? - | or3_intro2: P2 → or3 ? ? ? -. - -interpretation "multiple disjunction connective (3)" 'Or P0 P1 P2 = (or3 P0 P1 P2). - -(* multiple disjunction connective (4) *) - -inductive or4 (P0,P1,P2,P3:Prop) : Prop ≝ - | or4_intro0: P0 → or4 ? ? ? ? - | or4_intro1: P1 → or4 ? ? ? ? - | or4_intro2: P2 → or4 ? ? ? ? - | or4_intro3: P3 → or4 ? ? ? ? -. - -interpretation "multiple disjunction connective (4)" 'Or P0 P1 P2 P3 = (or4 P0 P1 P2 P3). - -(* multiple disjunction connective (5) *) - -inductive or5 (P0,P1,P2,P3,P4:Prop) : Prop ≝ - | or5_intro0: P0 → or5 ? ? ? ? ? - | or5_intro1: P1 → or5 ? ? ? ? ? - | or5_intro2: P2 → or5 ? ? ? ? ? - | or5_intro3: P3 → or5 ? ? ? ? ? - | or5_intro4: P4 → or5 ? ? ? ? ? -. - -interpretation "multiple disjunction connective (5)" 'Or P0 P1 P2 P3 P4 = (or5 P0 P1 P2 P3 P4). - -(* multiple conjunction connective (3) *) - -inductive and3 (P0,P1,P2:Prop) : Prop ≝ - | and3_intro: P0 → P1 → P2 → and3 ? ? ? -. - -interpretation "multiple conjunction connective (3)" 'And P0 P1 P2 = (and3 P0 P1 P2). - -(* multiple conjunction connective (4) *) - -inductive and4 (P0,P1,P2,P3:Prop) : Prop ≝ - | and4_intro: P0 → P1 → P2 → P3 → and4 ? ? ? ? -. - -interpretation "multiple conjunction connective (4)" 'And P0 P1 P2 P3 = (and4 P0 P1 P2 P3). - diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma new file mode 100644 index 000000000..a4281da4a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma @@ -0,0 +1,293 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +include "basics/pts.ma". + +include "ground_2/notation/xoa_notation.ma". + +(* multiple existental quantifier (1, 2) *) + +inductive ex1_2 (A0,A1:Type[0]) (P0:A0→A1→Prop) : Prop ≝ + | ex1_2_intro: ∀x0,x1. P0 x0 x1 → ex1_2 ? ? ? +. + +interpretation "multiple existental quantifier (1, 2)" 'Ex P0 = (ex1_2 ? ? P0). + +(* multiple existental quantifier (1, 3) *) + +inductive ex1_3 (A0,A1,A2:Type[0]) (P0:A0→A1→A2→Prop) : Prop ≝ + | ex1_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → ex1_3 ? ? ? ? +. + +interpretation "multiple existental quantifier (1, 3)" 'Ex P0 = (ex1_3 ? ? ? P0). + +(* multiple existental quantifier (2, 2) *) + +inductive ex2_2 (A0,A1:Type[0]) (P0,P1:A0→A1→Prop) : Prop ≝ + | ex2_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → ex2_2 ? ? ? ? +. + +interpretation "multiple existental quantifier (2, 2)" 'Ex P0 P1 = (ex2_2 ? ? P0 P1). + +(* multiple existental quantifier (2, 3) *) + +inductive ex2_3 (A0,A1,A2:Type[0]) (P0,P1:A0→A1→A2→Prop) : Prop ≝ + | ex2_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → ex2_3 ? ? ? ? ? +. + +interpretation "multiple existental quantifier (2, 3)" 'Ex P0 P1 = (ex2_3 ? ? ? P0 P1). + +(* multiple existental quantifier (3, 1) *) + +inductive ex3 (A0:Type[0]) (P0,P1,P2:A0→Prop) : Prop ≝ + | ex3_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → ex3 ? ? ? ? +. + +interpretation "multiple existental quantifier (3, 1)" 'Ex P0 P1 P2 = (ex3 ? P0 P1 P2). + +(* multiple existental quantifier (3, 2) *) + +inductive ex3_2 (A0,A1:Type[0]) (P0,P1,P2:A0→A1→Prop) : Prop ≝ + | ex3_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → P2 x0 x1 → ex3_2 ? ? ? ? ? +. + +interpretation "multiple existental quantifier (3, 2)" 'Ex P0 P1 P2 = (ex3_2 ? ? P0 P1 P2). + +(* multiple existental quantifier (3, 3) *) + +inductive ex3_3 (A0,A1,A2:Type[0]) (P0,P1,P2:A0→A1→A2→Prop) : Prop ≝ + | ex3_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → ex3_3 ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (3, 3)" 'Ex P0 P1 P2 = (ex3_3 ? ? ? P0 P1 P2). + +(* multiple existental quantifier (3, 4) *) + +inductive ex3_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2:A0→A1→A2→A3→Prop) : Prop ≝ + | ex3_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → ex3_4 ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (3, 4)" 'Ex P0 P1 P2 = (ex3_4 ? ? ? ? P0 P1 P2). + +(* multiple existental quantifier (4, 1) *) + +inductive ex4 (A0:Type[0]) (P0,P1,P2,P3:A0→Prop) : Prop ≝ + | ex4_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → P3 x0 → ex4 ? ? ? ? ? +. + +interpretation "multiple existental quantifier (4, 1)" 'Ex P0 P1 P2 P3 = (ex4 ? P0 P1 P2 P3). + +(* multiple existental quantifier (4, 2) *) + +inductive ex4_2 (A0,A1:Type[0]) (P0,P1,P2,P3:A0→A1→Prop) : Prop ≝ + | ex4_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → P2 x0 x1 → P3 x0 x1 → ex4_2 ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (4, 2)" 'Ex P0 P1 P2 P3 = (ex4_2 ? ? P0 P1 P2 P3). + +(* multiple existental quantifier (4, 3) *) + +inductive ex4_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3:A0→A1→A2→Prop) : Prop ≝ + | ex4_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → ex4_3 ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (4, 3)" 'Ex P0 P1 P2 P3 = (ex4_3 ? ? ? P0 P1 P2 P3). + +(* multiple existental quantifier (4, 4) *) + +inductive ex4_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3:A0→A1→A2→A3→Prop) : Prop ≝ + | ex4_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → ex4_4 ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (4, 4)" 'Ex P0 P1 P2 P3 = (ex4_4 ? ? ? ? P0 P1 P2 P3). + +(* multiple existental quantifier (4, 5) *) + +inductive ex4_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3:A0→A1→A2→A3→A4→Prop) : Prop ≝ + | ex4_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → ex4_5 ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (4, 5)" 'Ex P0 P1 P2 P3 = (ex4_5 ? ? ? ? ? P0 P1 P2 P3). + +(* multiple existental quantifier (5, 2) *) + +inductive ex5_2 (A0,A1:Type[0]) (P0,P1,P2,P3,P4:A0→A1→Prop) : Prop ≝ + | ex5_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → P2 x0 x1 → P3 x0 x1 → P4 x0 x1 → ex5_2 ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (5, 2)" 'Ex P0 P1 P2 P3 P4 = (ex5_2 ? ? P0 P1 P2 P3 P4). + +(* multiple existental quantifier (5, 3) *) + +inductive ex5_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→Prop) : Prop ≝ + | ex5_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → P4 x0 x1 x2 → ex5_3 ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (5, 3)" 'Ex P0 P1 P2 P3 P4 = (ex5_3 ? ? ? P0 P1 P2 P3 P4). + +(* multiple existental quantifier (5, 4) *) + +inductive ex5_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→A3→Prop) : Prop ≝ + | ex5_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → ex5_4 ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (5, 4)" 'Ex P0 P1 P2 P3 P4 = (ex5_4 ? ? ? ? P0 P1 P2 P3 P4). + +(* multiple existental quantifier (5, 5) *) + +inductive ex5_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→A3→A4→Prop) : Prop ≝ + | ex5_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → P4 x0 x1 x2 x3 x4 → ex5_5 ? ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (5, 5)" 'Ex P0 P1 P2 P3 P4 = (ex5_5 ? ? ? ? ? P0 P1 P2 P3 P4). + +(* multiple existental quantifier (5, 6) *) + +inductive ex5_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→A3→A4→A5→Prop) : Prop ≝ + | ex5_6_intro: ∀x0,x1,x2,x3,x4,x5. P0 x0 x1 x2 x3 x4 x5 → P1 x0 x1 x2 x3 x4 x5 → P2 x0 x1 x2 x3 x4 x5 → P3 x0 x1 x2 x3 x4 x5 → P4 x0 x1 x2 x3 x4 x5 → ex5_6 ? ? ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (5, 6)" 'Ex P0 P1 P2 P3 P4 = (ex5_6 ? ? ? ? ? ? P0 P1 P2 P3 P4). + +(* multiple existental quantifier (6, 3) *) + +inductive ex6_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→Prop) : Prop ≝ + | ex6_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → P4 x0 x1 x2 → P5 x0 x1 x2 → ex6_3 ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (6, 3)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_3 ? ? ? P0 P1 P2 P3 P4 P5). + +(* multiple existental quantifier (6, 4) *) + +inductive ex6_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→Prop) : Prop ≝ + | ex6_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → P5 x0 x1 x2 x3 → ex6_4 ? ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (6, 4)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_4 ? ? ? ? P0 P1 P2 P3 P4 P5). + +(* multiple existental quantifier (6, 5) *) + +inductive ex6_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→A4→Prop) : Prop ≝ + | ex6_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → P4 x0 x1 x2 x3 x4 → P5 x0 x1 x2 x3 x4 → ex6_5 ? ? ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (6, 5)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_5 ? ? ? ? ? P0 P1 P2 P3 P4 P5). + +(* multiple existental quantifier (6, 6) *) + +inductive ex6_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→A4→A5→Prop) : Prop ≝ + | ex6_6_intro: ∀x0,x1,x2,x3,x4,x5. P0 x0 x1 x2 x3 x4 x5 → P1 x0 x1 x2 x3 x4 x5 → P2 x0 x1 x2 x3 x4 x5 → P3 x0 x1 x2 x3 x4 x5 → P4 x0 x1 x2 x3 x4 x5 → P5 x0 x1 x2 x3 x4 x5 → ex6_6 ? ? ? ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (6, 6)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_6 ? ? ? ? ? ? P0 P1 P2 P3 P4 P5). + +(* multiple existental quantifier (6, 7) *) + +inductive ex6_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→A4→A5→A6→Prop) : Prop ≝ + | ex6_7_intro: ∀x0,x1,x2,x3,x4,x5,x6. P0 x0 x1 x2 x3 x4 x5 x6 → P1 x0 x1 x2 x3 x4 x5 x6 → P2 x0 x1 x2 x3 x4 x5 x6 → P3 x0 x1 x2 x3 x4 x5 x6 → P4 x0 x1 x2 x3 x4 x5 x6 → P5 x0 x1 x2 x3 x4 x5 x6 → ex6_7 ? ? ? ? ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (6, 7)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5). + +(* multiple existental quantifier (7, 4) *) + +inductive ex7_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→Prop) : Prop ≝ + | ex7_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → P5 x0 x1 x2 x3 → P6 x0 x1 x2 x3 → ex7_4 ? ? ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (7, 4)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6). + +(* multiple existental quantifier (7, 7) *) + +inductive ex7_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→A5→A6→Prop) : Prop ≝ + | ex7_7_intro: ∀x0,x1,x2,x3,x4,x5,x6. P0 x0 x1 x2 x3 x4 x5 x6 → P1 x0 x1 x2 x3 x4 x5 x6 → P2 x0 x1 x2 x3 x4 x5 x6 → P3 x0 x1 x2 x3 x4 x5 x6 → P4 x0 x1 x2 x3 x4 x5 x6 → P5 x0 x1 x2 x3 x4 x5 x6 → P6 x0 x1 x2 x3 x4 x5 x6 → ex7_7 ? ? ? ? ? ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (7, 7)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6). + +(* multiple existental quantifier (8, 5) *) + +inductive ex8_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3,P4,P5,P6,P7:A0→A1→A2→A3→A4→Prop) : Prop ≝ + | ex8_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → P4 x0 x1 x2 x3 x4 → P5 x0 x1 x2 x3 x4 → P6 x0 x1 x2 x3 x4 → P7 x0 x1 x2 x3 x4 → ex8_5 ? ? ? ? ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (8, 5)" 'Ex P0 P1 P2 P3 P4 P5 P6 P7 = (ex8_5 ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6 P7). + +(* multiple existental quantifier (9, 3) *) + +inductive ex9_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4,P5,P6,P7,P8:A0→A1→A2→Prop) : Prop ≝ + | ex9_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → P4 x0 x1 x2 → P5 x0 x1 x2 → P6 x0 x1 x2 → P7 x0 x1 x2 → P8 x0 x1 x2 → ex9_3 ? ? ? ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (9, 3)" 'Ex P0 P1 P2 P3 P4 P5 P6 P7 P8 = (ex9_3 ? ? ? P0 P1 P2 P3 P4 P5 P6 P7 P8). + +(* multiple existental quantifier (10, 4) *) + +inductive ex10_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5,P6,P7,P8,P9:A0→A1→A2→A3→Prop) : Prop ≝ + | ex10_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → P5 x0 x1 x2 x3 → P6 x0 x1 x2 x3 → P7 x0 x1 x2 x3 → P8 x0 x1 x2 x3 → P9 x0 x1 x2 x3 → ex10_4 ? ? ? ? ? ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (10, 4)" 'Ex P0 P1 P2 P3 P4 P5 P6 P7 P8 P9 = (ex10_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6 P7 P8 P9). + +(* multiple disjunction connective (3) *) + +inductive or3 (P0,P1,P2:Prop) : Prop ≝ + | or3_intro0: P0 → or3 ? ? ? + | or3_intro1: P1 → or3 ? ? ? + | or3_intro2: P2 → or3 ? ? ? +. + +interpretation "multiple disjunction connective (3)" 'Or P0 P1 P2 = (or3 P0 P1 P2). + +(* multiple disjunction connective (4) *) + +inductive or4 (P0,P1,P2,P3:Prop) : Prop ≝ + | or4_intro0: P0 → or4 ? ? ? ? + | or4_intro1: P1 → or4 ? ? ? ? + | or4_intro2: P2 → or4 ? ? ? ? + | or4_intro3: P3 → or4 ? ? ? ? +. + +interpretation "multiple disjunction connective (4)" 'Or P0 P1 P2 P3 = (or4 P0 P1 P2 P3). + +(* multiple disjunction connective (5) *) + +inductive or5 (P0,P1,P2,P3,P4:Prop) : Prop ≝ + | or5_intro0: P0 → or5 ? ? ? ? ? + | or5_intro1: P1 → or5 ? ? ? ? ? + | or5_intro2: P2 → or5 ? ? ? ? ? + | or5_intro3: P3 → or5 ? ? ? ? ? + | or5_intro4: P4 → or5 ? ? ? ? ? +. + +interpretation "multiple disjunction connective (5)" 'Or P0 P1 P2 P3 P4 = (or5 P0 P1 P2 P3 P4). + +(* multiple conjunction connective (3) *) + +inductive and3 (P0,P1,P2:Prop) : Prop ≝ + | and3_intro: P0 → P1 → P2 → and3 ? ? ? +. + +interpretation "multiple conjunction connective (3)" 'And P0 P1 P2 = (and3 P0 P1 P2). + +(* multiple conjunction connective (4) *) + +inductive and4 (P0,P1,P2,P3:Prop) : Prop ≝ + | and4_intro: P0 → P1 → P2 → P3 → and4 ? ? ? ? +. + +interpretation "multiple conjunction connective (4)" 'And P0 P1 P2 P3 = (and4 P0 P1 P2 P3). + diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa_props.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa_props.ma new file mode 100644 index 000000000..e917bacd2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa_props.ma @@ -0,0 +1,22 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "basics/logic.ma". +include "ground_2/notation/xoa/false_0.ma". +include "ground_2/notation/xoa/true_0.ma". +include "ground_2/xoa/xoa.ma". + +interpretation "logical false" 'false = False. + +interpretation "logical true" 'true = True. diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa_notation.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa_notation.ma deleted file mode 100644 index 753fc2712..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa_notation.ma +++ /dev/null @@ -1,326 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -(* This file was generated by xoa.native: do not edit *********************) - -(* multiple existental quantifier (1, 2) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.$P0) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) }. - -(* multiple existental quantifier (1, 3) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) }. - -(* multiple existental quantifier (2, 2) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.$P0) (λ${ident x0}.λ${ident x1}.$P1) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) }. - -(* multiple existental quantifier (2, 3) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) }. - -(* multiple existental quantifier (3, 1) *) - -notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.$P0) (λ${ident x0}.$P1) (λ${ident x0}.$P2) }. - -notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) (λ${ident x0}:$T0.$P2) }. - -(* multiple existental quantifier (3, 2) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.$P0) (λ${ident x0}.λ${ident x1}.$P1) (λ${ident x0}.λ${ident x1}.$P2) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P2) }. - -(* multiple existental quantifier (3, 3) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) }. - -(* multiple existental quantifier (3, 4) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) }. - -(* multiple existental quantifier (4, 1) *) - -notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.$P0) (λ${ident x0}.$P1) (λ${ident x0}.$P2) (λ${ident x0}.$P3) }. - -notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) (λ${ident x0}:$T0.$P2) (λ${ident x0}:$T0.$P3) }. - -(* multiple existental quantifier (4, 2) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.$P0) (λ${ident x0}.λ${ident x1}.$P1) (λ${ident x0}.λ${ident x1}.$P2) (λ${ident x0}.λ${ident x1}.$P3) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P3) }. - -(* multiple existental quantifier (4, 3) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P3) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) }. - -(* multiple existental quantifier (4, 4) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P3) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) }. - -(* multiple existental quantifier (4, 5) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P3) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) }. - -(* multiple existental quantifier (5, 2) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.$P0) (λ${ident x0}.λ${ident x1}.$P1) (λ${ident x0}.λ${ident x1}.$P2) (λ${ident x0}.λ${ident x1}.$P3) (λ${ident x0}.λ${ident x1}.$P4) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P4) }. - -(* multiple existental quantifier (5, 3) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P4) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P4) }. - -(* multiple existental quantifier (5, 4) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P4) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) }. - -(* multiple existental quantifier (5, 5) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P4) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P4) }. - -(* multiple existental quantifier (5, 6) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P4) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P4) }. - -(* multiple existental quantifier (6, 3) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P5) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P5) }. - -(* multiple existental quantifier (6, 4) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P5) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P5) }. - -(* multiple existental quantifier (6, 5) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P5) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P5) }. - -(* multiple existental quantifier (6, 6) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P5) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P5) }. - -(* multiple existental quantifier (6, 7) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P5) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P5) }. - -(* multiple existental quantifier (7, 4) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P6) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P6) }. - -(* multiple existental quantifier (7, 7) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P6) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P6) }. - -(* multiple existental quantifier (8, 5) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P6) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P7) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P6) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P7) }. - -(* multiple existental quantifier (9, 3) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7 break & term 19 P8)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P6) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P7) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P8) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7 break & term 19 P8)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P6) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P7) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P8) }. - -(* multiple existental quantifier (10, 4) *) - -notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7 break & term 19 P8 break & term 19 P9)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P6) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P7) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P8) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P9) }. - -notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7 break & term 19 P8 break & term 19 P9)" - non associative with precedence 20 - for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P6) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P7) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P8) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P9) }. - -(* multiple disjunction connective (3) *) - -notation "hvbox(∨∨ term 29 P0 break | term 29 P1 break | term 29 P2)" - non associative with precedence 30 - for @{ 'Or $P0 $P1 $P2 }. - -(* multiple disjunction connective (4) *) - -notation "hvbox(∨∨ term 29 P0 break | term 29 P1 break | term 29 P2 break | term 29 P3)" - non associative with precedence 30 - for @{ 'Or $P0 $P1 $P2 $P3 }. - -(* multiple disjunction connective (5) *) - -notation "hvbox(∨∨ term 29 P0 break | term 29 P1 break | term 29 P2 break | term 29 P3 break | term 29 P4)" - non associative with precedence 30 - for @{ 'Or $P0 $P1 $P2 $P3 $P4 }. - -(* multiple conjunction connective (3) *) - -notation "hvbox(∧∧ term 34 P0 break & term 34 P1 break & term 34 P2)" - non associative with precedence 35 - for @{ 'And $P0 $P1 $P2 }. - -(* multiple conjunction connective (4) *) - -notation "hvbox(∧∧ term 34 P0 break & term 34 P1 break & term 34 P2 break & term 34 P3)" - non associative with precedence 35 - for @{ 'And $P0 $P1 $P2 $P3 }. - diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa_props.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa_props.ma deleted file mode 100644 index 06bfbc739..000000000 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa_props.ma +++ /dev/null @@ -1,21 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 "basics/logic.ma". -include "ground_2/xoa_notation.ma". -include "ground_2/xoa.ma". - -interpretation "logical false" 'false = False. - -interpretation "logical true" 'true = True. diff --git a/matita/matita/lib/lambda/background/preamble.ma b/matita/matita/lib/lambda/background/preamble.ma index a4400abce..6a087e3aa 100644 --- a/matita/matita/lib/lambda/background/preamble.ma +++ b/matita/matita/lib/lambda/background/preamble.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basics/star.ma". +include "basics/star1.ma". include "basics/lists/lstar.ma". include "arithmetics/exp.ma". diff --git a/matita/matita/lib/lambda/background/xoa.ma b/matita/matita/lib/lambda/background/xoa.ma index a2f19a6b7..96a1fb95c 100644 --- a/matita/matita/lib/lambda/background/xoa.ma +++ b/matita/matita/lib/lambda/background/xoa.ma @@ -16,6 +16,8 @@ include "basics/pts.ma". +include "lambda/background/xoa_notation.ma". + (* multiple existental quantifier (1, 2) *) inductive ex1_2 (A0,A1:Type[0]) (P0:A0→A1→Prop) : Prop ≝ diff --git a/matita/matita/lib/lambda/xoa.conf.xml b/matita/matita/lib/lambda/xoa.conf.xml index 04cbcf59e..2d188536d 100644 --- a/matita/matita/lib/lambda/xoa.conf.xml +++ b/matita/matita/lib/lambda/xoa.conf.xml @@ -4,9 +4,9 @@ $(MATITA_RT_BASE_DIR)
- contribs/lambda/background/ - xoa - xoa_notation + lib/ + lambda/background/xoa + lambda/background/xoa_notation basics/pts.ma 1 2 2 2