From: Ferruccio Guidi Date: Sun, 28 Feb 2021 19:54:43 +0000 (+0100) Subject: update in ground X-Git-Tag: make_still_working~154 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ca318d6d92098c3a65c9f0841174ca110c82e064;p=helm.git update in ground + xoa restyled + missing files committed --- diff --git a/matita/components/binaries/xoa/engine.ml b/matita/components/binaries/xoa/engine.ml index baf460c09..47770e710 100644 --- a/matita/components/binaries/xoa/engine.ml +++ b/matita/components/binaries/xoa/engine.ml @@ -70,22 +70,22 @@ let mk_exists ooch noch c v = let full b n = P.sprintf "(%s.$P%u)" (abst_clo b) (c - n) in let full_seq b = string_iter " " (full b) c in - P.fprintf ooch "(* %s (%u, %u) *)\n\n" description c v; + P.fprintf ooch "(* Note: %s (%u, %u) *)\n" description c v; P.fprintf ooch "inductive %s (%s:Type[0]) (%s:%s→Prop) : Prop ≝\n" o_name set_list pre_list set_type; - P.fprintf ooch " | %s_intro: ∀%s. %s → %s %s %s\n.\n\n" + P.fprintf ooch " | %s_intro: ∀%s. %s → %s %s %s\n.\n\n" o_name ele_list pre_type o_name qm_set qm_pre; P.fprintf ooch "interpretation \"%s (%u, %u)\" %s %s = (%s %s %s).\n\n" description c v i_name pre_seq o_name qm_set pre_seq; - P.fprintf noch "(* %s (%u, %u) *)\n\n" description c v; + P.fprintf noch "(* Note: %s (%u, %u) *)\n" description c v; - P.fprintf noch "notation > \"hvbox(∃∃ %s break . %s)\"\n %s for @{ %s %s }.\n\n" + P.fprintf noch "notation > \"hvbox(∃∃ %s break . %s)\"\n %s for @{ %s %s }.\n\n" id_list term_conj prec i_name (full_seq false); - P.fprintf noch "notation < \"hvbox(∃∃ %s break . %s)\"\n %s for @{ %s %s }.\n\n" + P.fprintf noch "notation < \"hvbox(∃∃ %s break . %s)\"\n %s for @{ %s %s }.\n\n" id_list term_conj prec i_name (full_seq true) let mk_or ooch noch c = @@ -108,11 +108,11 @@ let mk_or ooch noch c = let par n = P.sprintf "$P%u" (c - n) in let par_seq = string_iter " " par c in - let mk_con n = P.fprintf ooch " | %s_intro%u: %s → %s %s\n" + let mk_con n = P.fprintf ooch " | %s_intro%u: %s → %s %s\n" o_name (c - n) (pre n) o_name qm_pre in - P.fprintf ooch "(* %s (%u) *)\n\n" description c; + P.fprintf ooch "(* Note: %s (%u) *)\n" description c; P.fprintf ooch "inductive %s (%s:Prop) : Prop ≝\n" o_name pre_list; @@ -122,9 +122,9 @@ let mk_or ooch noch c = P.fprintf ooch "interpretation \"%s (%u)\" %s %s = (%s %s).\n\n" description c i_name pre_seq o_name pre_seq; - P.fprintf noch "(* %s (%u) *)\n\n" description c; + P.fprintf noch "(* Note: %s (%u) *)\n" description c; - P.fprintf noch "notation \"hvbox(∨∨ %s)\"\n %s for @{ %s %s }.\n\n" + P.fprintf noch "notation \"hvbox(∨∨ %s)\"\n %s for @{ %s %s }.\n\n" term_disj prec i_name par_seq let mk_and ooch noch c = @@ -148,19 +148,19 @@ let mk_and ooch noch c = let par n = P.sprintf "$P%u" (c - n) in let par_seq = string_iter " " par c in - P.fprintf ooch "(* %s (%u) *)\n\n" description c; + P.fprintf ooch "(* Note: %s (%u) *)\n" description c; P.fprintf ooch "inductive %s (%s:Prop) : Prop ≝\n" o_name pre_list; - P.fprintf ooch " | %s_intro: %s → %s %s\n.\n\n" + P.fprintf ooch " | %s_intro: %s → %s %s\n.\n\n" o_name pre_type o_name qm_pre; P.fprintf ooch "interpretation \"%s (%u)\" %s %s = (%s %s).\n\n" description c i_name pre_seq o_name pre_seq; - P.fprintf noch "(* %s (%u) *)\n\n" description c; + P.fprintf noch "(* Note: %s (%u) *)\n" description c; - P.fprintf noch "notation \"hvbox(∧∧ %s)\"\n %s for @{ %s %s }.\n\n" + P.fprintf noch "notation \"hvbox(∧∧ %s)\"\n %s for @{ %s %s }.\n\n" term_conj prec i_name par_seq let generate ooch noch = function diff --git a/matita/components/binaries/xoa/lib.ml b/matita/components/binaries/xoa/lib.ml index ec9ec81d2..f2bf31757 100644 --- a/matita/components/binaries/xoa/lib.ml +++ b/matita/components/binaries/xoa/lib.ml @@ -30,9 +30,15 @@ let copy_preamble preamble och = in try read () with End_of_file -> close_in ich +let print_header def och = + let msg = if def then "LOGIC" else "GROUND NOTATION" in + let stars = String.make (72 - String.length msg) '*' in + Printf.fprintf och "(* %s %s*)\n\n" msg stars + let print_comment och = - let stars = String.make (30 - String.length myself) '*' in - Printf.fprintf och "(* This file was generated by %s: do not edit %s*)\n\n" myself stars + let msg = Printf.sprintf "NOTE: This file was generated by %s, do not edit" myself in + let stars = String.make (72 - String.length msg) '*' in + Printf.fprintf och "(* %s %s*)\n\n" msg stars let exists_out name = let path = [ @@ -42,14 +48,16 @@ let exists_out name = let name = List.fold_left F.concat "" path in K.file_exists (name ^ ".ma") -let open_out preamble name = +let open_out def preamble name = let path = [ R.get_string "xoa.output_dir"; name ] in let name = List.fold_left F.concat "" path in let och = open_out (name ^ ".ma") in - copy_preamble preamble och; print_comment och; + copy_preamble preamble och; + print_header def och; + print_comment och; och let out_include och s = diff --git a/matita/components/binaries/xoa/lib.mli b/matita/components/binaries/xoa/lib.mli index 0c81d2425..cc66968d3 100644 --- a/matita/components/binaries/xoa/lib.mli +++ b/matita/components/binaries/xoa/lib.mli @@ -13,6 +13,6 @@ val get_preamble: string -> string val exists_out: string -> bool -val open_out: string -> string -> out_channel +val open_out: bool -> string -> string -> out_channel val out_include: out_channel -> string -> unit diff --git a/matita/components/binaries/xoa/xoa.ml b/matita/components/binaries/xoa/xoa.ml index c5604f1e6..64ce87b17 100644 --- a/matita/components/binaries/xoa/xoa.ml +++ b/matita/components/binaries/xoa/xoa.ml @@ -35,8 +35,8 @@ let unm_and s = let process_centralized conf = let preamble = L.get_preamble conf in if R.has "xoa.objects" && R.has "xoa.notations" then begin - let ooch = L.open_out preamble (R.get_string "xoa.objects") in - let noch = L.open_out preamble (R.get_string "xoa.notations") in + let ooch = L.open_out true preamble (R.get_string "xoa.objects") in + let noch = L.open_out false 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"); @@ -62,8 +62,8 @@ let generate (p, o, n) d = in if !incremental && L.exists_out oname && L.exists_out nname then () else begin - let ooch = L.open_out p oname in - let noch = L.open_out p nname in + let ooch = L.open_out true p oname in + let noch = L.open_out false p nname in List.iter (L.out_include ooch) (R.get_list R.string "xoa.include"); L.out_include ooch (nname ^ ".ma"); E.generate ooch noch d; diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/bGroundLib.mrc b/matita/matita/contribs/lambdadelta/bin/recomm/bGroundLib.mrc index fdc932735..78ef1dd35 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/bGroundLib.mrc +++ b/matita/matita/contribs/lambdadelta/bin/recomm/bGroundLib.mrc @@ -1,4 +1,5 @@ PcsAnd b "" true false +ex4 eq land lsub diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundLib.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundLib.ml index 94db88ed7..1402aff57 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundLib.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommGcbGroundLib.ml @@ -11,6 +11,7 @@ let step k st outs ins = | "lsub" :: tl -> k T.OK ("lsub" :: outs) tl | "land" :: tl -> k T.OK ("land" :: outs) tl | "eq" :: tl -> k T.OK ("eq" :: outs) tl + | "ex4" :: tl -> k T.OK ("ex4" :: outs) tl | _ -> k T.OO outs ins let main = diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma index d4d8be1e3..c2d89a6f7 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground/insert_eq/insert_eq_1.ma". +include "ground/generated/insert_eq_1.ma". include "ground/arith/nat_succ.ma". (* ORDER FOR NON-NEGATIVE INTEGERS ******************************************) diff --git a/matita/matita/contribs/lambdadelta/ground/counters/rtc.ma b/matita/matita/contribs/lambdadelta/ground/counters/rtc.ma index 414fa1bfe..5e055b787 100644 --- a/matita/matita/contribs/lambdadelta/ground/counters/rtc.ma +++ b/matita/matita/contribs/lambdadelta/ground/counters/rtc.ma @@ -17,7 +17,7 @@ include "ground/notation/functions/tuple_4.ma". include "ground/notation/functions/zerozero_0.ma". include "ground/notation/functions/zeroone_0.ma". include "ground/notation/functions/onezero_0.ma". -include "ground/insert_eq/insert_eq_1.ma". +include "ground/generated/insert_eq_1.ma". include "ground/arith/nat.ma". (* RT-TRANSITION COUNTERS ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/ground/lib/ltc.ma b/matita/matita/contribs/lambdadelta/ground/lib/ltc.ma index c0d091c3c..9c2e12a7a 100644 --- a/matita/matita/contribs/lambdadelta/ground/lib/ltc.ma +++ b/matita/matita/contribs/lambdadelta/ground/lib/ltc.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground/insert_eq/insert_eq_1.ma". +include "ground/generated/insert_eq_1.ma". include "ground/lib/functions.ma". (* LABELLED TRANSITIVE CLOSURE FOR RELATIONS ********************************) diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/and_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/and_3.ma index 03b0e7e29..34cc5ec64 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/and_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/and_3.ma @@ -12,11 +12,12 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple conjunction connective (3) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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 }. + non associative with precedence 35 + for @{ 'And $P0 $P1 $P2 }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/and_4.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/and_4.ma index 78c1f9963..073550fc2 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/and_4.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/and_4.ma @@ -12,11 +12,12 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple conjunction connective (4) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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 }. + non associative with precedence 35 + for @{ 'And $P0 $P1 $P2 $P3 }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_1_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_1_2.ma index 77c7366a6..ea0484b16 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_1_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_1_2.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (1, 2) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: multiple existental quantifier (1, 2) *) notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0)" - non associative with precedence 20 - for @{ 'Ex2 (λ${ident x0}.λ${ident x1}.$P0) }. + non associative with precedence 20 + for @{ 'Ex2 (λ${ident x0}.λ${ident x1}.$P0) }. notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0)" - non associative with precedence 20 - for @{ 'Ex2 (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) }. + non associative with precedence 20 + for @{ 'Ex2 (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_1_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_1_3.ma index 89cc727bf..4067fc500 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_1_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_1_3.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (1, 3) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: multiple existental quantifier (1, 3) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0)" - non associative with precedence 20 - for @{ 'Ex3 (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) }. + non associative with precedence 20 + for @{ 'Ex3 (λ${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 @{ 'Ex3 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) }. + non associative with precedence 20 + for @{ 'Ex3 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_1_4.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_1_4.ma index 0fbf2a458..b509f87c2 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_1_4.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_1_4.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (1, 4) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: multiple existental quantifier (1, 4) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0)" - non associative with precedence 20 - for @{ 'Ex4 (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) }. + non associative with precedence 20 + for @{ 'Ex4 (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) }. notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0)" - non associative with precedence 20 - for @{ 'Ex4 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) }. + non associative with precedence 20 + for @{ 'Ex4 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_2_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_2_2.ma index ccef16288..fa15afef1 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_2_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_2_2.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (2, 2) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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 @{ 'Ex2 (λ${ident x0}.λ${ident x1}.$P0) (λ${ident x0}.λ${ident x1}.$P1) }. + non associative with precedence 20 + for @{ 'Ex2 (λ${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 @{ 'Ex2 (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) }. + non associative with precedence 20 + for @{ 'Ex2 (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_2_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_2_3.ma index 5e0dba550..937e6dde8 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_2_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_2_3.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (2, 3) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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 @{ 'Ex3 (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) }. + non associative with precedence 20 + for @{ 'Ex3 (λ${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 @{ 'Ex3 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) }. + non associative with precedence 20 + for @{ 'Ex3 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_3_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_3_1.ma index f5c367157..ddd2b4edf 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_3_1.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_3_1.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (3, 1) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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) }. + 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) }. + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) (λ${ident x0}:$T0.$P2) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_3_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_3_2.ma index 8ca34d307..905f65f5f 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_3_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_3_2.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (3, 2) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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 @{ 'Ex2 (λ${ident x0}.λ${ident x1}.$P0) (λ${ident x0}.λ${ident x1}.$P1) (λ${ident x0}.λ${ident x1}.$P2) }. + non associative with precedence 20 + for @{ 'Ex2 (λ${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 @{ 'Ex2 (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P2) }. + non associative with precedence 20 + for @{ 'Ex2 (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P2) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_3_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_3_3.ma index 6287d1a4e..62b08889b 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_3_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_3_3.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (3, 3) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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 @{ 'Ex3 (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) }. + non associative with precedence 20 + for @{ 'Ex3 (λ${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 @{ 'Ex3 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex3 (λ${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) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_3_4.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_3_4.ma index 5f34348e3..1e11b5452 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_3_4.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_3_4.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (3, 4) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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 @{ 'Ex4 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex4 (λ${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 @{ 'Ex4 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex4 (λ${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) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_3_5.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_3_5.ma index fab03970d..3d506b778 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_3_5.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_3_5.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (3, 5) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: multiple existental quantifier (3, 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)" - non associative with precedence 20 - for @{ 'Ex5 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex5 (λ${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) }. notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2)" - non associative with precedence 20 - for @{ 'Ex5 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex5 (λ${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) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_3_6.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_3_6.ma index 1dd1986dc..fac6d1b52 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_3_6.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_3_6.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (3, 6) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: multiple existental quantifier (3, 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)" - non associative with precedence 20 - for @{ 'Ex6 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex6 (λ${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) }. 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)" - non associative with precedence 20 - for @{ 'Ex6 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex6 (λ${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) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_4_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_4_1.ma index 75ac29f16..4c1e8ccd6 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_4_1.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_4_1.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (4, 1) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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) }. + 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) }. + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) (λ${ident x0}:$T0.$P2) (λ${ident x0}:$T0.$P3) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_4_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_4_2.ma index e8a6e9650..c6de2348c 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_4_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_4_2.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (4, 2) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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 @{ 'Ex2 (λ${ident x0}.λ${ident x1}.$P0) (λ${ident x0}.λ${ident x1}.$P1) (λ${ident x0}.λ${ident x1}.$P2) (λ${ident x0}.λ${ident x1}.$P3) }. + non associative with precedence 20 + for @{ 'Ex2 (λ${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 @{ 'Ex2 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex2 (λ${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) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_4_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_4_3.ma index 2d52220e2..e6f0dce91 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_4_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_4_3.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (4, 3) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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 @{ 'Ex3 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex3 (λ${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 @{ 'Ex3 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex3 (λ${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) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_4_4.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_4_4.ma index 9ab7a12d0..596c01575 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_4_4.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_4_4.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (4, 4) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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 @{ 'Ex4 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex4 (λ${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 @{ 'Ex4 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex4 (λ${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) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_4_5.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_4_5.ma index ab7b80d49..094fc87c5 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_4_5.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_4_5.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (4, 5) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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 @{ 'Ex5 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex5 (λ${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 @{ 'Ex5 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex5 (λ${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) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_5_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_5_1.ma index a31168095..b4cd7cb0f 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_5_1.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_5_1.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (5, 1) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: multiple existental quantifier (5, 1) *) notation > "hvbox(∃∃ ident x0 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}.$P0) (λ${ident x0}.$P1) (λ${ident x0}.$P2) (λ${ident x0}.$P3) (λ${ident x0}.$P4) }. + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.$P0) (λ${ident x0}.$P1) (λ${ident x0}.$P2) (λ${ident x0}.$P3) (λ${ident x0}.$P4) }. notation < "hvbox(∃∃ ident x0 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.$P0) (λ${ident x0}:$T0.$P1) (λ${ident x0}:$T0.$P2) (λ${ident x0}:$T0.$P3) (λ${ident x0}:$T0.$P4) }. + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) (λ${ident x0}:$T0.$P2) (λ${ident x0}:$T0.$P3) (λ${ident x0}:$T0.$P4) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_5_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_5_2.ma index 52b614c19..7d4c51829 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_5_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_5_2.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (5, 2) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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 @{ 'Ex2 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex2 (λ${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 @{ 'Ex2 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex2 (λ${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) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_5_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_5_3.ma index f4a01f23a..0c898cb46 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_5_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_5_3.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (5, 3) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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 @{ 'Ex3 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex3 (λ${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 @{ 'Ex3 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex3 (λ${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) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_5_4.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_5_4.ma index 59e8cb89b..42060b050 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_5_4.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_5_4.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (5, 4) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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 @{ 'Ex4 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex4 (λ${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 @{ 'Ex4 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex4 (λ${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) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_5_5.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_5_5.ma index 704b9de00..0aa288c86 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_5_5.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_5_5.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (5, 5) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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 @{ 'Ex5 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex5 (λ${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 @{ 'Ex5 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex5 (λ${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) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_5_6.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_5_6.ma index d5dd2806c..610d926f9 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_5_6.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_5_6.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (5, 6) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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 @{ 'Ex6 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex6 (λ${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 @{ 'Ex6 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex6 (λ${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) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_5_7.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_5_7.ma index fb2986fbc..8e2a39314 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_5_7.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_5_7.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (5, 7) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: multiple existental quantifier (5, 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)" - non associative with precedence 20 - for @{ 'Ex7 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex7 (λ${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) }. 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)" - non associative with precedence 20 - for @{ 'Ex7 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex7 (λ${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) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_6_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_6_3.ma index 33dcc0d31..5b79263e8 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_6_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_6_3.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (6, 3) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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 @{ 'Ex3 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex3 (λ${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 @{ 'Ex3 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex3 (λ${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) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_6_4.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_6_4.ma index 5b0aae453..c4622f7f2 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_6_4.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_6_4.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (6, 4) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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 @{ 'Ex4 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex4 (λ${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 @{ 'Ex4 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex4 (λ${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) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_6_5.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_6_5.ma index 962185ec2..626c867a8 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_6_5.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_6_5.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (6, 5) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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 @{ 'Ex5 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex5 (λ${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 @{ 'Ex5 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex5 (λ${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) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_6_6.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_6_6.ma index e3351ba35..34f7d7b89 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_6_6.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_6_6.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (6, 6) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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 @{ 'Ex6 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex6 (λ${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 @{ 'Ex6 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex6 (λ${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) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_6_7.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_6_7.ma index a699be8e9..0ccfefdbf 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_6_7.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_6_7.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (6, 7) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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 @{ 'Ex7 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex7 (λ${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 @{ 'Ex7 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex7 (λ${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) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_6_8.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_6_8.ma index b7ba4f5c2..b97e01634 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_6_8.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_6_8.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (6, 8) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: multiple existental quantifier (6, 8) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 , ident x7 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 @{ 'Ex8 (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P5) }. + non associative with precedence 20 + for @{ 'Ex8 (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.$P5) }. notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 , ident x7 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 @{ 'Ex8 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P5) }. + non associative with precedence 20 + for @{ 'Ex8 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.$P5) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_6_9.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_6_9.ma index c7d473828..37ee50383 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_6_9.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_6_9.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (6, 9) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: multiple existental quantifier (6, 9) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 , ident x7 , ident x8 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 @{ 'Ex9 (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.λ${ident x8}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.λ${ident x8}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.λ${ident x8}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.λ${ident x8}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.λ${ident x8}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.λ${ident x8}.$P5) }. + non associative with precedence 20 + for @{ 'Ex9 (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.λ${ident x8}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.λ${ident x8}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.λ${ident x8}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.λ${ident x8}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.λ${ident x8}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.λ${ident x8}.$P5) }. notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 , ident x7 , ident x8 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 @{ 'Ex9 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.λ${ident x8}:$T8.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.λ${ident x8}:$T8.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.λ${ident x8}:$T8.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.λ${ident x8}:$T8.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.λ${ident x8}:$T8.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.λ${ident x8}:$T8.$P5) }. + non associative with precedence 20 + for @{ 'Ex9 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.λ${ident x8}:$T8.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.λ${ident x8}:$T8.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.λ${ident x8}:$T8.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.λ${ident x8}:$T8.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.λ${ident x8}:$T8.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.λ${ident x8}:$T8.$P5) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_7_10.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_7_10.ma index d6285b86b..6cfc8147b 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_7_10.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_7_10.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (7, 10) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: multiple existental quantifier (7, 10) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 , ident x7 , ident x8 , ident x9 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 @{ 'Ex10 (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.λ${ident x8}.λ${ident x9}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.λ${ident x8}.λ${ident x9}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.λ${ident x8}.λ${ident x9}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.λ${ident x8}.λ${ident x9}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.λ${ident x8}.λ${ident x9}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.λ${ident x8}.λ${ident x9}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.λ${ident x8}.λ${ident x9}.$P6) }. + non associative with precedence 20 + for @{ 'Ex10 (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.λ${ident x8}.λ${ident x9}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.λ${ident x8}.λ${ident x9}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.λ${ident x8}.λ${ident x9}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.λ${ident x8}.λ${ident x9}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.λ${ident x8}.λ${ident x9}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.λ${ident x8}.λ${ident x9}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.λ${ident x7}.λ${ident x8}.λ${ident x9}.$P6) }. notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 , ident x7 , ident x8 , ident x9 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 @{ 'Ex10 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.λ${ident x8}:$T8.λ${ident x9}:$T9.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.λ${ident x8}:$T8.λ${ident x9}:$T9.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.λ${ident x8}:$T8.λ${ident x9}:$T9.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.λ${ident x8}:$T8.λ${ident x9}:$T9.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.λ${ident x8}:$T8.λ${ident x9}:$T9.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.λ${ident x8}:$T8.λ${ident x9}:$T9.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.λ${ident x8}:$T8.λ${ident x9}:$T9.$P6) }. + non associative with precedence 20 + for @{ 'Ex10 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.λ${ident x8}:$T8.λ${ident x9}:$T9.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.λ${ident x8}:$T8.λ${ident x9}:$T9.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.λ${ident x8}:$T8.λ${ident x9}:$T9.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.λ${ident x8}:$T8.λ${ident x9}:$T9.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.λ${ident x8}:$T8.λ${ident x9}:$T9.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.λ${ident x8}:$T8.λ${ident x9}:$T9.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.λ${ident x7}:$T7.λ${ident x8}:$T8.λ${ident x9}:$T9.$P6) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_7_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_7_3.ma index 35cf4ecc8..32b4b0c88 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_7_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_7_3.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (7, 3) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: multiple existental quantifier (7, 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)" - non associative with precedence 20 - for @{ 'Ex3 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex3 (λ${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) }. 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)" - non associative with precedence 20 - for @{ 'Ex3 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex3 (λ${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) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_7_4.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_7_4.ma index b40af123a..090ca20c1 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_7_4.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_7_4.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (7, 4) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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 @{ 'Ex4 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex4 (λ${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 @{ 'Ex4 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex4 (λ${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) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_7_5.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_7_5.ma index 4ec1b7cce..272ddd4ec 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_7_5.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_7_5.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (7, 5) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: multiple existental quantifier (7, 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)" - non associative with precedence 20 - for @{ 'Ex5 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex5 (λ${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) }. 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)" - non associative with precedence 20 - for @{ 'Ex5 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex5 (λ${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) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_7_6.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_7_6.ma index 24892462d..f8f41f6dc 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_7_6.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_7_6.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (7, 6) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: multiple existental quantifier (7, 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 break & term 19 P6)" - non associative with precedence 20 - for @{ 'Ex6 (λ${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) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P6) }. + non associative with precedence 20 + for @{ 'Ex6 (λ${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) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.$P6) }. 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 break & term 19 P6)" - non associative with precedence 20 - for @{ 'Ex6 (λ${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) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P6) }. + non associative with precedence 20 + for @{ 'Ex6 (λ${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) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P6) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_7_7.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_7_7.ma index 9be29b5c1..edf40f888 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_7_7.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_7_7.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (7, 7) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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 @{ 'Ex7 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex7 (λ${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 @{ 'Ex7 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex7 (λ${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) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_8_4.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_8_4.ma index baa422aaf..7e5044fc3 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_8_4.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_8_4.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (8, 4) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: multiple existental quantifier (8, 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)" - non associative with precedence 20 - for @{ 'Ex4 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex4 (λ${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) }. 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)" - non associative with precedence 20 - for @{ 'Ex4 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex4 (λ${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) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_8_5.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_8_5.ma index 8a7bb8f14..1f6a99fd1 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_8_5.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_8_5.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (8, 5) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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 @{ 'Ex5 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex5 (λ${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 @{ 'Ex5 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex5 (λ${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) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_9_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_9_3.ma index 609f6974d..576aef540 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_9_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/ex_9_3.ma @@ -12,15 +12,16 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple existental quantifier (9, 3) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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 @{ 'Ex3 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex3 (λ${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 @{ 'Ex3 (λ${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) }. + non associative with precedence 20 + for @{ 'Ex3 (λ${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) }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/or_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/or_3.ma index 3f8265443..4e1bfcb00 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/or_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/or_3.ma @@ -12,11 +12,12 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple disjunction connective (3) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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 }. + non associative with precedence 30 + for @{ 'Or $P0 $P1 $P2 }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/or_4.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/or_4.ma index 5d5be50a4..06ad07c32 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/or_4.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/or_4.ma @@ -12,11 +12,12 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple disjunction connective (4) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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 }. + non associative with precedence 30 + for @{ 'Or $P0 $P1 $P2 $P3 }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/xoa/or_5.ma b/matita/matita/contribs/lambdadelta/ground/notation/xoa/or_5.ma index 7f558933e..217458c80 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/xoa/or_5.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/xoa/or_5.ma @@ -12,11 +12,12 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* GROUND NOTATION **********************************************************) -(* multiple disjunction connective (5) *) +(* NOTE: This file was generated by xoa.native, do not edit *****************) +(* Note: 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 }. + non associative with precedence 30 + for @{ 'Or $P0 $P1 $P2 $P3 $P4 }. diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/and_3.ma b/matita/matita/contribs/lambdadelta/ground/xoa/and_3.ma index f99e0da9d..28c57ae69 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/and_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/and_3.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/and_3.ma". -(* multiple conjunction connective (3) *) - +(* Note: multiple conjunction connective (3) *) inductive and3 (P0,P1,P2:Prop) : Prop ≝ - | and3_intro: P0 → P1 → P2 → and3 ? ? ? + | and3_intro: P0 → P1 → P2 → and3 ? ? ? . interpretation "multiple conjunction connective (3)" 'And P0 P1 P2 = (and3 P0 P1 P2). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/and_4.ma b/matita/matita/contribs/lambdadelta/ground/xoa/and_4.ma index aeee4617f..a9046d38b 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/and_4.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/and_4.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/and_4.ma". -(* multiple conjunction connective (4) *) - +(* Note: multiple conjunction connective (4) *) inductive and4 (P0,P1,P2,P3:Prop) : Prop ≝ - | and4_intro: P0 → P1 → P2 → P3 → and4 ? ? ? ? + | 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/xoa/ex_1_2.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_1_2.ma index 0d6b9e4f2..5a14aff29 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_1_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_1_2.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_1_2.ma". -(* multiple existental quantifier (1, 2) *) - +(* Note: 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 ? ? ? + | ex1_2_intro: ∀x0,x1. P0 x0 x1 → ex1_2 ? ? ? . interpretation "multiple existental quantifier (1, 2)" 'Ex2 P0 = (ex1_2 ? ? P0). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_1_3.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_1_3.ma index 7e195cd3a..4ca475a88 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_1_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_1_3.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_1_3.ma". -(* multiple existental quantifier (1, 3) *) - +(* Note: 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 ? ? ? ? + | ex1_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → ex1_3 ? ? ? ? . interpretation "multiple existental quantifier (1, 3)" 'Ex3 P0 = (ex1_3 ? ? ? P0). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_1_4.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_1_4.ma index 77f1dd696..026b64c0e 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_1_4.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_1_4.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_1_4.ma". -(* multiple existental quantifier (1, 4) *) - +(* Note: multiple existental quantifier (1, 4) *) inductive ex1_4 (A0,A1,A2,A3:Type[0]) (P0:A0→A1→A2→A3→Prop) : Prop ≝ - | ex1_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → ex1_4 ? ? ? ? ? + | ex1_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → ex1_4 ? ? ? ? ? . interpretation "multiple existental quantifier (1, 4)" 'Ex4 P0 = (ex1_4 ? ? ? ? P0). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_2_2.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_2_2.ma index 055cee51a..3914c7327 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_2_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_2_2.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_2_2.ma". -(* multiple existental quantifier (2, 2) *) - +(* Note: 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 ? ? ? ? + | ex2_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → ex2_2 ? ? ? ? . interpretation "multiple existental quantifier (2, 2)" 'Ex2 P0 P1 = (ex2_2 ? ? P0 P1). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_2_3.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_2_3.ma index bcbee747a..8dffc414f 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_2_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_2_3.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_2_3.ma". -(* multiple existental quantifier (2, 3) *) - +(* Note: 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 ? ? ? ? ? + | ex2_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → ex2_3 ? ? ? ? ? . interpretation "multiple existental quantifier (2, 3)" 'Ex3 P0 P1 = (ex2_3 ? ? ? P0 P1). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_3_1.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_3_1.ma index 3ce615636..9a2d0636b 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_3_1.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_3_1.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_3_1.ma". -(* multiple existental quantifier (3, 1) *) - +(* Note: 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 ? ? ? ? + | ex3_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → ex3 ? ? ? ? . interpretation "multiple existental quantifier (3, 1)" 'Ex P0 P1 P2 = (ex3 ? P0 P1 P2). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_3_2.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_3_2.ma index e7fc185d1..ba37987f3 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_3_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_3_2.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_3_2.ma". -(* multiple existental quantifier (3, 2) *) - +(* Note: 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 ? ? ? ? ? + | ex3_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → P2 x0 x1 → ex3_2 ? ? ? ? ? . interpretation "multiple existental quantifier (3, 2)" 'Ex2 P0 P1 P2 = (ex3_2 ? ? P0 P1 P2). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_3_3.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_3_3.ma index cfa954454..032132877 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_3_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_3_3.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_3_3.ma". -(* multiple existental quantifier (3, 3) *) - +(* Note: 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 ? ? ? ? ? ? + | 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)" 'Ex3 P0 P1 P2 = (ex3_3 ? ? ? P0 P1 P2). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_3_4.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_3_4.ma index 672102b2e..7d06290f2 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_3_4.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_3_4.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_3_4.ma". -(* multiple existental quantifier (3, 4) *) - +(* Note: 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 ? ? ? ? ? ? ? + | 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)" 'Ex4 P0 P1 P2 = (ex3_4 ? ? ? ? P0 P1 P2). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_3_5.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_3_5.ma index e1fa69fbf..7db84b905 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_3_5.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_3_5.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_3_5.ma". -(* multiple existental quantifier (3, 5) *) - +(* Note: multiple existental quantifier (3, 5) *) inductive ex3_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2:A0→A1→A2→A3→A4→Prop) : Prop ≝ - | ex3_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 → ex3_5 ? ? ? ? ? ? ? ? + | ex3_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 → ex3_5 ? ? ? ? ? ? ? ? . interpretation "multiple existental quantifier (3, 5)" 'Ex5 P0 P1 P2 = (ex3_5 ? ? ? ? ? P0 P1 P2). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_3_6.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_3_6.ma index ccef1fd88..07b008807 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_3_6.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_3_6.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_3_6.ma". -(* multiple existental quantifier (3, 6) *) - +(* Note: multiple existental quantifier (3, 6) *) inductive ex3_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2:A0→A1→A2→A3→A4→A5→Prop) : Prop ≝ - | ex3_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 → ex3_6 ? ? ? ? ? ? ? ? ? + | ex3_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 → ex3_6 ? ? ? ? ? ? ? ? ? . interpretation "multiple existental quantifier (3, 6)" 'Ex6 P0 P1 P2 = (ex3_6 ? ? ? ? ? ? P0 P1 P2). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_1.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_1.ma index 055f6954d..bdf6274dd 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_1.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_1.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_4_1.ma". -(* multiple existental quantifier (4, 1) *) - +(* Note: 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 ? ? ? ? ? + | 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). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_1_props.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_1_props.ma index e13197cb0..03a20b092 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_1_props.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_1_props.ma @@ -12,9 +12,11 @@ (* *) (**************************************************************************) +(* LOGIC ********************************************************************) + include "ground/xoa/ex_4_1.ma". -(* Properties with multiple existental quantifier (4, 1) ********************) +(* Constructions with ex4 ***************************************************) lemma ex4_commute (A0) (P0,P1,P2,P3:A0→Prop): (∃∃x0. P0 x0 & P1 x0 & P2 x0 & P3 x0) → ∃∃x0. P2 x0 & P3 x0 & P0 x0 & P1 x0. diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_2.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_2.ma index 288fa6c90..665ace69d 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_2.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_4_2.ma". -(* multiple existental quantifier (4, 2) *) - +(* Note: 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 ? ? ? ? ? ? + | 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)" 'Ex2 P0 P1 P2 P3 = (ex4_2 ? ? P0 P1 P2 P3). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_3.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_3.ma index 6c9e5ce61..0def4c186 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_3.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_4_3.ma". -(* multiple existental quantifier (4, 3) *) - +(* Note: 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 ? ? ? ? ? ? ? + | 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)" 'Ex3 P0 P1 P2 P3 = (ex4_3 ? ? ? P0 P1 P2 P3). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_4.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_4.ma index 775ce5840..a0208b524 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_4.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_4.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_4_4.ma". -(* multiple existental quantifier (4, 4) *) - +(* Note: 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 ? ? ? ? ? ? ? ? + | 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)" 'Ex4 P0 P1 P2 P3 = (ex4_4 ? ? ? ? P0 P1 P2 P3). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_5.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_5.ma index 4f3cd76c1..7b49117ae 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_5.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_5.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_4_5.ma". -(* multiple existental quantifier (4, 5) *) - +(* Note: 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 ? ? ? ? ? ? ? ? ? + | 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)" 'Ex5 P0 P1 P2 P3 = (ex4_5 ? ? ? ? ? P0 P1 P2 P3). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_5_1.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_5_1.ma index af0e36ebc..422e55fff 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_5_1.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_5_1.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_5_1.ma". -(* multiple existental quantifier (5, 1) *) - +(* Note: multiple existental quantifier (5, 1) *) inductive ex5 (A0:Type[0]) (P0,P1,P2,P3,P4:A0→Prop) : Prop ≝ - | ex5_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → P3 x0 → P4 x0 → ex5 ? ? ? ? ? ? + | ex5_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → P3 x0 → P4 x0 → ex5 ? ? ? ? ? ? . interpretation "multiple existental quantifier (5, 1)" 'Ex P0 P1 P2 P3 P4 = (ex5 ? P0 P1 P2 P3 P4). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_5_2.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_5_2.ma index 80dff2b36..b82115ada 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_5_2.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_5_2.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_5_2.ma". -(* multiple existental quantifier (5, 2) *) - +(* Note: 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 ? ? ? ? ? ? ? + | 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)" 'Ex2 P0 P1 P2 P3 P4 = (ex5_2 ? ? P0 P1 P2 P3 P4). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_5_3.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_5_3.ma index f476e84cb..bfb3f47e0 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_5_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_5_3.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_5_3.ma". -(* multiple existental quantifier (5, 3) *) - +(* Note: 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 ? ? ? ? ? ? ? ? + | 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)" 'Ex3 P0 P1 P2 P3 P4 = (ex5_3 ? ? ? P0 P1 P2 P3 P4). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_5_4.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_5_4.ma index 0ab21d1fa..35d2707e9 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_5_4.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_5_4.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_5_4.ma". -(* multiple existental quantifier (5, 4) *) - +(* Note: 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 ? ? ? ? ? ? ? ? ? + | 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)" 'Ex4 P0 P1 P2 P3 P4 = (ex5_4 ? ? ? ? P0 P1 P2 P3 P4). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_5_5.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_5_5.ma index 45ff6c303..f8edd37c0 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_5_5.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_5_5.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_5_5.ma". -(* multiple existental quantifier (5, 5) *) - +(* Note: 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 ? ? ? ? ? ? ? ? ? ? + | 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)" 'Ex5 P0 P1 P2 P3 P4 = (ex5_5 ? ? ? ? ? P0 P1 P2 P3 P4). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_5_6.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_5_6.ma index 35d154c56..dc0e71461 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_5_6.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_5_6.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_5_6.ma". -(* multiple existental quantifier (5, 6) *) - +(* Note: 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 ? ? ? ? ? ? ? ? ? ? ? + | 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)" 'Ex6 P0 P1 P2 P3 P4 = (ex5_6 ? ? ? ? ? ? P0 P1 P2 P3 P4). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_5_7.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_5_7.ma index b35818aa4..fc57503f1 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_5_7.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_5_7.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_5_7.ma". -(* multiple existental quantifier (5, 7) *) - +(* Note: multiple existental quantifier (5, 7) *) inductive ex5_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→A3→A4→A5→A6→Prop) : Prop ≝ - | ex5_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 → ex5_7 ? ? ? ? ? ? ? ? ? ? ? ? + | ex5_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 → ex5_7 ? ? ? ? ? ? ? ? ? ? ? ? . interpretation "multiple existental quantifier (5, 7)" 'Ex7 P0 P1 P2 P3 P4 = (ex5_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_6_3.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_6_3.ma index 27e0824b3..044bad6aa 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_6_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_6_3.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_6_3.ma". -(* multiple existental quantifier (6, 3) *) - +(* Note: 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 ? ? ? ? ? ? ? ? ? + | 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)" 'Ex3 P0 P1 P2 P3 P4 P5 = (ex6_3 ? ? ? P0 P1 P2 P3 P4 P5). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_6_4.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_6_4.ma index 374f4997d..fcd982802 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_6_4.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_6_4.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_6_4.ma". -(* multiple existental quantifier (6, 4) *) - +(* Note: 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 ? ? ? ? ? ? ? ? ? ? + | 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)" 'Ex4 P0 P1 P2 P3 P4 P5 = (ex6_4 ? ? ? ? P0 P1 P2 P3 P4 P5). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_6_5.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_6_5.ma index b68890ba8..1c3c3c2b8 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_6_5.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_6_5.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_6_5.ma". -(* multiple existental quantifier (6, 5) *) - +(* Note: 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 ? ? ? ? ? ? ? ? ? ? ? + | 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)" 'Ex5 P0 P1 P2 P3 P4 P5 = (ex6_5 ? ? ? ? ? P0 P1 P2 P3 P4 P5). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_6_6.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_6_6.ma index 17f909431..cede71816 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_6_6.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_6_6.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_6_6.ma". -(* multiple existental quantifier (6, 6) *) - +(* Note: 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 ? ? ? ? ? ? ? ? ? ? ? ? + | 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)" 'Ex6 P0 P1 P2 P3 P4 P5 = (ex6_6 ? ? ? ? ? ? P0 P1 P2 P3 P4 P5). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_6_7.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_6_7.ma index 48f53406e..5874fafd1 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_6_7.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_6_7.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_6_7.ma". -(* multiple existental quantifier (6, 7) *) - +(* Note: 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 ? ? ? ? ? ? ? ? ? ? ? ? ? + | 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)" 'Ex7 P0 P1 P2 P3 P4 P5 = (ex6_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_6_8.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_6_8.ma index 811b39f04..26116abec 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_6_8.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_6_8.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_6_8.ma". -(* multiple existental quantifier (6, 8) *) - +(* Note: multiple existental quantifier (6, 8) *) inductive ex6_8 (A0,A1,A2,A3,A4,A5,A6,A7:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→A4→A5→A6→A7→Prop) : Prop ≝ - | ex6_8_intro: ∀x0,x1,x2,x3,x4,x5,x6,x7. P0 x0 x1 x2 x3 x4 x5 x6 x7 → P1 x0 x1 x2 x3 x4 x5 x6 x7 → P2 x0 x1 x2 x3 x4 x5 x6 x7 → P3 x0 x1 x2 x3 x4 x5 x6 x7 → P4 x0 x1 x2 x3 x4 x5 x6 x7 → P5 x0 x1 x2 x3 x4 x5 x6 x7 → ex6_8 ? ? ? ? ? ? ? ? ? ? ? ? ? ? + | ex6_8_intro: ∀x0,x1,x2,x3,x4,x5,x6,x7. P0 x0 x1 x2 x3 x4 x5 x6 x7 → P1 x0 x1 x2 x3 x4 x5 x6 x7 → P2 x0 x1 x2 x3 x4 x5 x6 x7 → P3 x0 x1 x2 x3 x4 x5 x6 x7 → P4 x0 x1 x2 x3 x4 x5 x6 x7 → P5 x0 x1 x2 x3 x4 x5 x6 x7 → ex6_8 ? ? ? ? ? ? ? ? ? ? ? ? ? ? . interpretation "multiple existental quantifier (6, 8)" 'Ex8 P0 P1 P2 P3 P4 P5 = (ex6_8 ? ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_6_9.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_6_9.ma index f94349580..7afc586ea 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_6_9.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_6_9.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_6_9.ma". -(* multiple existental quantifier (6, 9) *) - +(* Note: multiple existental quantifier (6, 9) *) inductive ex6_9 (A0,A1,A2,A3,A4,A5,A6,A7,A8:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→A4→A5→A6→A7→A8→Prop) : Prop ≝ - | ex6_9_intro: ∀x0,x1,x2,x3,x4,x5,x6,x7,x8. P0 x0 x1 x2 x3 x4 x5 x6 x7 x8 → P1 x0 x1 x2 x3 x4 x5 x6 x7 x8 → P2 x0 x1 x2 x3 x4 x5 x6 x7 x8 → P3 x0 x1 x2 x3 x4 x5 x6 x7 x8 → P4 x0 x1 x2 x3 x4 x5 x6 x7 x8 → P5 x0 x1 x2 x3 x4 x5 x6 x7 x8 → ex6_9 ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? + | ex6_9_intro: ∀x0,x1,x2,x3,x4,x5,x6,x7,x8. P0 x0 x1 x2 x3 x4 x5 x6 x7 x8 → P1 x0 x1 x2 x3 x4 x5 x6 x7 x8 → P2 x0 x1 x2 x3 x4 x5 x6 x7 x8 → P3 x0 x1 x2 x3 x4 x5 x6 x7 x8 → P4 x0 x1 x2 x3 x4 x5 x6 x7 x8 → P5 x0 x1 x2 x3 x4 x5 x6 x7 x8 → ex6_9 ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? . interpretation "multiple existental quantifier (6, 9)" 'Ex9 P0 P1 P2 P3 P4 P5 = (ex6_9 ? ? ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_7_10.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_7_10.ma index f3e001c26..5946e4334 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_7_10.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_7_10.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_7_10.ma". -(* multiple existental quantifier (7, 10) *) - +(* Note: multiple existental quantifier (7, 10) *) inductive ex7_10 (A0,A1,A2,A3,A4,A5,A6,A7,A8,A9:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→A5→A6→A7→A8→A9→Prop) : Prop ≝ - | ex7_10_intro: ∀x0,x1,x2,x3,x4,x5,x6,x7,x8,x9. P0 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 → P1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 → P2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 → P3 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 → P4 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 → P5 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 → P6 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 → ex7_10 ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? + | ex7_10_intro: ∀x0,x1,x2,x3,x4,x5,x6,x7,x8,x9. P0 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 → P1 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 → P2 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 → P3 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 → P4 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 → P5 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 → P6 x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 → ex7_10 ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? . interpretation "multiple existental quantifier (7, 10)" 'Ex10 P0 P1 P2 P3 P4 P5 P6 = (ex7_10 ? ? ? ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_7_3.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_7_3.ma index 96eee3e68..01a0c2f57 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_7_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_7_3.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_7_3.ma". -(* multiple existental quantifier (7, 3) *) - +(* Note: multiple existental quantifier (7, 3) *) inductive ex7_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→Prop) : Prop ≝ - | ex7_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 → ex7_3 ? ? ? ? ? ? ? ? ? ? + | ex7_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 → ex7_3 ? ? ? ? ? ? ? ? ? ? . interpretation "multiple existental quantifier (7, 3)" 'Ex3 P0 P1 P2 P3 P4 P5 P6 = (ex7_3 ? ? ? P0 P1 P2 P3 P4 P5 P6). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_7_4.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_7_4.ma index 15316cda4..39d253fef 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_7_4.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_7_4.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_7_4.ma". -(* multiple existental quantifier (7, 4) *) - +(* Note: 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 ? ? ? ? ? ? ? ? ? ? ? + | 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)" 'Ex4 P0 P1 P2 P3 P4 P5 P6 = (ex7_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_7_5.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_7_5.ma index 89794476a..5139d3408 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_7_5.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_7_5.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_7_5.ma". -(* multiple existental quantifier (7, 5) *) - +(* Note: multiple existental quantifier (7, 5) *) inductive ex7_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→Prop) : Prop ≝ - | ex7_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 → ex7_5 ? ? ? ? ? ? ? ? ? ? ? ? + | ex7_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 → ex7_5 ? ? ? ? ? ? ? ? ? ? ? ? . interpretation "multiple existental quantifier (7, 5)" 'Ex5 P0 P1 P2 P3 P4 P5 P6 = (ex7_5 ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_7_6.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_7_6.ma index f6ea7b068..ccc5e71c5 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_7_6.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_7_6.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_7_6.ma". -(* multiple existental quantifier (7, 6) *) - +(* Note: multiple existental quantifier (7, 6) *) inductive ex7_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→A5→Prop) : Prop ≝ - | ex7_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 → P6 x0 x1 x2 x3 x4 x5 → ex7_6 ? ? ? ? ? ? ? ? ? ? ? ? ? + | ex7_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 → P6 x0 x1 x2 x3 x4 x5 → ex7_6 ? ? ? ? ? ? ? ? ? ? ? ? ? . interpretation "multiple existental quantifier (7, 6)" 'Ex6 P0 P1 P2 P3 P4 P5 P6 = (ex7_6 ? ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_7_7.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_7_7.ma index 688fd96f0..066aa437a 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_7_7.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_7_7.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_7_7.ma". -(* multiple existental quantifier (7, 7) *) - +(* Note: 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 ? ? ? ? ? ? ? ? ? ? ? ? ? ? + | 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)" 'Ex7 P0 P1 P2 P3 P4 P5 P6 = (ex7_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_8_4.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_8_4.ma index 680782088..292ff7b3d 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_8_4.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_8_4.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_8_4.ma". -(* multiple existental quantifier (8, 4) *) - +(* Note: multiple existental quantifier (8, 4) *) inductive ex8_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5,P6,P7:A0→A1→A2→A3→Prop) : Prop ≝ - | ex8_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 → ex8_4 ? ? ? ? ? ? ? ? ? ? ? ? + | ex8_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 → ex8_4 ? ? ? ? ? ? ? ? ? ? ? ? . interpretation "multiple existental quantifier (8, 4)" 'Ex4 P0 P1 P2 P3 P4 P5 P6 P7 = (ex8_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6 P7). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_8_5.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_8_5.ma index 31e65ee36..13447ab7d 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_8_5.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_8_5.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_8_5.ma". -(* multiple existental quantifier (8, 5) *) - +(* Note: 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 ? ? ? ? ? ? ? ? ? ? ? ? ? + | 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)" 'Ex5 P0 P1 P2 P3 P4 P5 P6 P7 = (ex8_5 ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6 P7). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_9_3.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_9_3.ma index 80e5c885b..332cfd7f7 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_9_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_9_3.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_9_3.ma". -(* multiple existental quantifier (9, 3) *) - +(* Note: 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 ? ? ? ? ? ? ? ? ? ? ? ? + | 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)" 'Ex3 P0 P1 P2 P3 P4 P5 P6 P7 P8 = (ex9_3 ? ? ? P0 P1 P2 P3 P4 P5 P6 P7 P8). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/or_3.ma b/matita/matita/contribs/lambdadelta/ground/xoa/or_3.ma index 77ddcdfe0..51e8f1cf8 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/or_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/or_3.ma @@ -12,18 +12,19 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/or_3.ma". -(* multiple disjunction connective (3) *) - +(* Note: multiple disjunction connective (3) *) inductive or3 (P0,P1,P2:Prop) : Prop ≝ - | or3_intro0: P0 → or3 ? ? ? - | or3_intro1: P1 → or3 ? ? ? - | or3_intro2: P2 → or3 ? ? ? + | 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). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/or_4.ma b/matita/matita/contribs/lambdadelta/ground/xoa/or_4.ma index e1d6a7b4f..11c7a209e 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/or_4.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/or_4.ma @@ -12,19 +12,20 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/or_4.ma". -(* multiple disjunction connective (4) *) - +(* Note: 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 ? ? ? ? + | 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). diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/or_5.ma b/matita/matita/contribs/lambdadelta/ground/xoa/or_5.ma index 98ea46816..b822801c8 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/or_5.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/or_5.ma @@ -12,20 +12,21 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/or_5.ma". -(* multiple disjunction connective (5) *) - +(* Note: 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 ? ? ? ? ? + | 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).