From e31ce850917b3e95f5158a687626c679e551fd25 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 18 Apr 2016 18:30:57 +0000 Subject: [PATCH] ground_2: generic rt-transition counter --- .../notation/constructors/onezero_0.ma | 19 +++ .../ground_2/notation/constructors/tuple_4.ma | 19 +++ .../notation/constructors/zeroone_0.ma | 19 +++ .../notation/constructors/zerozero_0.ma | 19 +++ .../ground_2/notation/xoa_notation.ma | 58 ++++----- .../lambdadelta/ground_2/steps/rtc.ma | 49 ++++++++ .../lambdadelta/ground_2/steps/rtc_plus.ma | 26 ++++ .../lambdadelta/ground_2/steps/rtc_shift.ma | 24 ++++ .../lambdadelta/ground_2/web/ground_2.ldw.xml | 3 + .../lambdadelta/ground_2/web/ground_2_src.tbl | 22 ++-- .../contribs/lambdadelta/ground_2/xoa/xoa.ma | 116 +++++++++--------- 11 files changed, 280 insertions(+), 94 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/constructors/onezero_0.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/constructors/tuple_4.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/constructors/zeroone_0.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/constructors/zerozero_0.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/steps/rtc.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/steps/rtc_shift.ma diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/onezero_0.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/onezero_0.ma new file mode 100644 index 000000000..5df776e6a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/onezero_0.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "𝟙𝟘" + non associative with precedence 55 + for @{ 'OneZero }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/tuple_4.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/tuple_4.ma new file mode 100644 index 000000000..551ee0d94 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/tuple_4.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "hvbox ( 〈 term 46 x1, break term 46 x2 , break term 46 x3, break term 46 x4 〉 )" + non associative with precedence 55 + for @{ 'Tuple $x1 $x2 $x3 $x4 }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/zeroone_0.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/zeroone_0.ma new file mode 100644 index 000000000..ff195abe1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/zeroone_0.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "𝟘𝟙" + non associative with precedence 55 + for @{ 'ZeroOne }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/zerozero_0.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/zerozero_0.ma new file mode 100644 index 000000000..cb4b10dad --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/zerozero_0.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "𝟘𝟘" + non associative with precedence 55 + for @{ 'ZeroZero }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/xoa_notation.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa_notation.ma index dd3338c01..e2555b3cf 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/notation/xoa_notation.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/xoa_notation.ma @@ -14,7 +14,7 @@ (* This file was generated by xoa.native: do not edit *********************) -(* multiple inductive existental quantifier (1, 2) *) +(* multiple existental quantifier (1, 2) *) notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0)" non associative with precedence 20 @@ -24,7 +24,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0)" non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) }. -(* multiple inductive existental quantifier (1, 3) *) +(* multiple existental quantifier (1, 3) *) notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0)" non associative with precedence 20 @@ -34,7 +34,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0)" non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) }. -(* multiple inductive existental quantifier (2, 2) *) +(* multiple existental quantifier (2, 2) *) notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1)" non associative with precedence 20 @@ -44,7 +44,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) }. -(* multiple inductive existental quantifier (2, 3) *) +(* 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 @@ -54,7 +54,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) }. -(* multiple inductive existental quantifier (3, 1) *) +(* 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 @@ -64,7 +64,7 @@ notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) (λ${ident x0}:$T0.$P2) }. -(* multiple inductive existental quantifier (3, 2) *) +(* 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 @@ -74,7 +74,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P2) }. -(* multiple inductive existental quantifier (3, 3) *) +(* 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 @@ -84,7 +84,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) }. -(* multiple inductive existental quantifier (3, 4) *) +(* 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 @@ -94,7 +94,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) }. -(* multiple inductive existental quantifier (3, 5) *) +(* 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 @@ -104,7 +104,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 br non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) }. -(* multiple inductive existental quantifier (4, 1) *) +(* 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 @@ -114,7 +114,7 @@ notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) (λ${ident x0}:$T0.$P2) (λ${ident x0}:$T0.$P3) }. -(* multiple inductive existental quantifier (4, 2) *) +(* 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 @@ -124,7 +124,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P3) }. -(* multiple inductive existental quantifier (4, 3) *) +(* 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 @@ -134,7 +134,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) }. -(* multiple inductive existental quantifier (4, 4) *) +(* 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 @@ -144,7 +144,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) }. -(* multiple inductive existental quantifier (4, 5) *) +(* 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 @@ -154,7 +154,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 br non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) }. -(* multiple inductive existental quantifier (5, 2) *) +(* 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 @@ -164,7 +164,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P4) }. -(* multiple inductive existental quantifier (5, 3) *) +(* 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 @@ -174,7 +174,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P4) }. -(* multiple inductive existental quantifier (5, 4) *) +(* 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 @@ -184,7 +184,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) }. -(* multiple inductive existental quantifier (5, 5) *) +(* 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 @@ -194,7 +194,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 br non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P4) }. -(* multiple inductive existental quantifier (5, 6) *) +(* 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 @@ -204,7 +204,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P4) }. -(* multiple inductive existental quantifier (6, 3) *) +(* 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 @@ -214,7 +214,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P5) }. -(* multiple inductive existental quantifier (6, 4) *) +(* 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 @@ -224,7 +224,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P5) }. -(* multiple inductive existental quantifier (6, 5) *) +(* 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 @@ -234,7 +234,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 br non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P5) }. -(* multiple inductive existental quantifier (6, 6) *) +(* 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 @@ -244,7 +244,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.$P5) }. -(* multiple inductive existental quantifier (6, 7) *) +(* 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 @@ -254,7 +254,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P5) }. -(* multiple inductive existental quantifier (7, 3) *) +(* 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 @@ -264,7 +264,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P6) }. -(* multiple inductive existental quantifier (7, 4) *) +(* 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 @@ -274,7 +274,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P6) }. -(* multiple inductive existental quantifier (7, 7) *) +(* 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 @@ -284,7 +284,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P6) }. -(* multiple inductive existental quantifier (8, 4) *) +(* 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 @@ -294,7 +294,7 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P6) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P7) }. -(* multiple inductive existental quantifier (8, 5) *) +(* 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 diff --git a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc.ma b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc.ma new file mode 100644 index 000000000..75960e4cb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc.ma @@ -0,0 +1,49 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground_2/notation/constructors/tuple_4.ma". +include "ground_2/notation/constructors/zerozero_0.ma". +include "ground_2/notation/constructors/zeroone_0.ma". +include "ground_2/notation/constructors/onezero_0.ma". +include "ground_2/lib/arith.ma". + +(* RT-TRANSITION COUNTER ****************************************************) + +record rtc: Type[0] ≝ { + ri: nat; (* Note: inner r-steps *) + rh: nat; (* Note: head r-steps *) + ti: nat; (* Note: inner t-steps *) + th: nat (* Note: head t-steps *) +}. + +interpretation "constructor (rtc)" + 'Tuple ri rh ti th = (mk_rtc ri rh ti th). + +(* Note: for one structural step *) +definition OO: rtc ≝ 〈0, 0, 0, 0〉. + +interpretation "one structural step (rtc)" + 'ZeroZero = (OO). + +(* Note: for one r-step *) +definition UO: rtc ≝ 〈0, 1, 0, 0〉. + +interpretation "one r-step (rtc)" + 'OneZero = (UO). + +(* Note: for one t-step *) +definition OU: rtc ≝ 〈0, 0, 0, 1〉. + +interpretation "one t-step (rtc)" + 'ZeroOne = (OU). diff --git a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma new file mode 100644 index 000000000..75a58b25f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_plus.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground_2/steps/rtc.ma". + +(* RT-TRANSITION COUNTER ****************************************************) + +definition plus (r1:rtc) (r2:rtc): rtc ≝ match r1 with [ + mk_rtc ri1 rh1 ti1 th1 ⇒ match r2 with [ + mk_rtc ri2 rh2 ti2 th2 ⇒ 〈ri1+ri2, rh1+rh2, ti1+ti2, th1+th2〉 + ] +]. + +interpretation "plus (rtc)" + 'plus r1 r2 = (plus r1 r2). diff --git a/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_shift.ma b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_shift.ma new file mode 100644 index 000000000..6cb0a8b1a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/steps/rtc_shift.ma @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground_2/notation/functions/drop_1.ma". +include "ground_2/steps/rtc.ma". + +(* RT-TRANSITION COUNTER ****************************************************) + +definition shift (r:rtc): rtc ≝ match r with +[ mk_rtc ri rh ti th ⇒ 〈ri+rh, 0, ti+th, 0〉 ]. + +interpretation "shift (rtc)" + 'Drop r = (shift r). diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml index 5b071cd95..f217a912f 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2.ldw.xml @@ -13,6 +13,9 @@ and its timeline. + + Generic rt-transition counter (rtc). + Platform-independent multiple relocation (rtmap). diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl index 9016bbd4f..8443ab81a 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl @@ -9,18 +9,15 @@ table { ] } ] - class "green" - [ { "natural numbers with infinity" * } { + class "water" + [ { "rt-transition counter" * } { [ { "" * } { - [ "ynat ( ∞ )" "ynat_pred ( ⫰? )" "ynat_succ ( ⫯? )" - "ynat_le ( ? ≤ ? )" "ynat_lt ( ? < ? )" - "ynat_plus ( ? + ? )" * - ] + [ "rtc ( 〈?,?,?,?〉 ) ( 𝟘𝟘 ) ( 𝟙𝟘 ) ( 𝟘𝟙 )" "rtc_shift ( ↓? )" "rtc_plus ( ? + ? )" * ] } ] } ] - class "grass" + class "green" [ { "multiple relocation" * } { [ { "" * } { [ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_tl ( ⫱? )" "rtmap_tls ( ⫱*[?]? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_fcla ( 𝐂⦃?⦄ ≡ ? )" "rtmap_isfin ( 𝐅⦃?⦄ )" "rtmap_isuni ( 𝐔⦃?⦄ )" "rtmap_uni ( 𝐔❴?❵ )" "rtmap_sle ( ? ⊆ ? )" "rtmap_sand ( ? ⋒ ? ≡ ? )" "rtmap_sor ( ? ⋓ ? ≡ ? )" "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≡ ? )" * ] @@ -34,6 +31,17 @@ table { ] } ] + class "grass" + [ { "natural numbers with infinity" * } { + [ { "" * } { + [ "ynat ( ∞ )" "ynat_pred ( ⫰? )" "ynat_succ ( ⫯? )" + "ynat_le ( ? ≤ ? )" "ynat_lt ( ? < ? )" + "ynat_plus ( ? + ? )" * + ] + } + ] + } + ] class "yellow" [ { "extensions to the library" * } { [ { "" * } { diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma index 7f46fe493..2fe6168ad 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa.ma @@ -18,237 +18,237 @@ include "basics/pts.ma". include "ground_2/notation/xoa_notation.ma". -(* multiple inductive existental quantifier (1, 2) *) +(* multiple existental quantifier (1, 2) *) inductive ex1_2 (A0,A1:Type[0]) (P0:A0→A1→Prop) : Prop ≝ | ex1_2_intro: ∀x0,x1. P0 x0 x1 → ex1_2 ? ? ? . -interpretation "multiple inductive existental quantifier (1, 2)" 'Ex P0 = (ex1_2 ? ? P0). +interpretation "multiple existental quantifier (1, 2)" 'Ex P0 = (ex1_2 ? ? P0). -(* multiple inductive existental quantifier (1, 3) *) +(* multiple existental quantifier (1, 3) *) inductive ex1_3 (A0,A1,A2:Type[0]) (P0:A0→A1→A2→Prop) : Prop ≝ | ex1_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → ex1_3 ? ? ? ? . -interpretation "multiple inductive existental quantifier (1, 3)" 'Ex P0 = (ex1_3 ? ? ? P0). +interpretation "multiple existental quantifier (1, 3)" 'Ex P0 = (ex1_3 ? ? ? P0). -(* multiple inductive existental quantifier (2, 2) *) +(* multiple existental quantifier (2, 2) *) inductive ex2_2 (A0,A1:Type[0]) (P0,P1:A0→A1→Prop) : Prop ≝ | ex2_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → ex2_2 ? ? ? ? . -interpretation "multiple inductive existental quantifier (2, 2)" 'Ex P0 P1 = (ex2_2 ? ? P0 P1). +interpretation "multiple existental quantifier (2, 2)" 'Ex P0 P1 = (ex2_2 ? ? P0 P1). -(* multiple inductive existental quantifier (2, 3) *) +(* multiple existental quantifier (2, 3) *) inductive ex2_3 (A0,A1,A2:Type[0]) (P0,P1:A0→A1→A2→Prop) : Prop ≝ | ex2_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → ex2_3 ? ? ? ? ? . -interpretation "multiple inductive existental quantifier (2, 3)" 'Ex P0 P1 = (ex2_3 ? ? ? P0 P1). +interpretation "multiple existental quantifier (2, 3)" 'Ex P0 P1 = (ex2_3 ? ? ? P0 P1). -(* multiple inductive existental quantifier (3, 1) *) +(* multiple existental quantifier (3, 1) *) inductive ex3 (A0:Type[0]) (P0,P1,P2:A0→Prop) : Prop ≝ | ex3_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → ex3 ? ? ? ? . -interpretation "multiple inductive existental quantifier (3, 1)" 'Ex P0 P1 P2 = (ex3 ? P0 P1 P2). +interpretation "multiple existental quantifier (3, 1)" 'Ex P0 P1 P2 = (ex3 ? P0 P1 P2). -(* multiple inductive existental quantifier (3, 2) *) +(* multiple existental quantifier (3, 2) *) inductive ex3_2 (A0,A1:Type[0]) (P0,P1,P2:A0→A1→Prop) : Prop ≝ | ex3_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → P2 x0 x1 → ex3_2 ? ? ? ? ? . -interpretation "multiple inductive existental quantifier (3, 2)" 'Ex P0 P1 P2 = (ex3_2 ? ? P0 P1 P2). +interpretation "multiple existental quantifier (3, 2)" 'Ex P0 P1 P2 = (ex3_2 ? ? P0 P1 P2). -(* multiple inductive existental quantifier (3, 3) *) +(* multiple existental quantifier (3, 3) *) inductive ex3_3 (A0,A1,A2:Type[0]) (P0,P1,P2:A0→A1→A2→Prop) : Prop ≝ | ex3_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → ex3_3 ? ? ? ? ? ? . -interpretation "multiple inductive existental quantifier (3, 3)" 'Ex P0 P1 P2 = (ex3_3 ? ? ? P0 P1 P2). +interpretation "multiple existental quantifier (3, 3)" 'Ex P0 P1 P2 = (ex3_3 ? ? ? P0 P1 P2). -(* multiple inductive existental quantifier (3, 4) *) +(* multiple existental quantifier (3, 4) *) inductive ex3_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2:A0→A1→A2→A3→Prop) : Prop ≝ | ex3_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → ex3_4 ? ? ? ? ? ? ? . -interpretation "multiple inductive existental quantifier (3, 4)" 'Ex P0 P1 P2 = (ex3_4 ? ? ? ? P0 P1 P2). +interpretation "multiple existental quantifier (3, 4)" 'Ex P0 P1 P2 = (ex3_4 ? ? ? ? P0 P1 P2). -(* multiple inductive existental quantifier (3, 5) *) +(* 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 ? ? ? ? ? ? ? ? . -interpretation "multiple inductive existental quantifier (3, 5)" 'Ex P0 P1 P2 = (ex3_5 ? ? ? ? ? P0 P1 P2). +interpretation "multiple existental quantifier (3, 5)" 'Ex P0 P1 P2 = (ex3_5 ? ? ? ? ? P0 P1 P2). -(* multiple inductive existental quantifier (4, 1) *) +(* multiple existental quantifier (4, 1) *) inductive ex4 (A0:Type[0]) (P0,P1,P2,P3:A0→Prop) : Prop ≝ | ex4_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → P3 x0 → ex4 ? ? ? ? ? . -interpretation "multiple inductive existental quantifier (4, 1)" 'Ex P0 P1 P2 P3 = (ex4 ? P0 P1 P2 P3). +interpretation "multiple existental quantifier (4, 1)" 'Ex P0 P1 P2 P3 = (ex4 ? P0 P1 P2 P3). -(* multiple inductive existental quantifier (4, 2) *) +(* multiple existental quantifier (4, 2) *) inductive ex4_2 (A0,A1:Type[0]) (P0,P1,P2,P3:A0→A1→Prop) : Prop ≝ | ex4_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → P2 x0 x1 → P3 x0 x1 → ex4_2 ? ? ? ? ? ? . -interpretation "multiple inductive existental quantifier (4, 2)" 'Ex P0 P1 P2 P3 = (ex4_2 ? ? P0 P1 P2 P3). +interpretation "multiple existental quantifier (4, 2)" 'Ex P0 P1 P2 P3 = (ex4_2 ? ? P0 P1 P2 P3). -(* multiple inductive existental quantifier (4, 3) *) +(* multiple existental quantifier (4, 3) *) inductive ex4_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3:A0→A1→A2→Prop) : Prop ≝ | ex4_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → ex4_3 ? ? ? ? ? ? ? . -interpretation "multiple inductive existental quantifier (4, 3)" 'Ex P0 P1 P2 P3 = (ex4_3 ? ? ? P0 P1 P2 P3). +interpretation "multiple existental quantifier (4, 3)" 'Ex P0 P1 P2 P3 = (ex4_3 ? ? ? P0 P1 P2 P3). -(* multiple inductive existental quantifier (4, 4) *) +(* multiple existental quantifier (4, 4) *) inductive ex4_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3:A0→A1→A2→A3→Prop) : Prop ≝ | ex4_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → ex4_4 ? ? ? ? ? ? ? ? . -interpretation "multiple inductive existental quantifier (4, 4)" 'Ex P0 P1 P2 P3 = (ex4_4 ? ? ? ? P0 P1 P2 P3). +interpretation "multiple existental quantifier (4, 4)" 'Ex P0 P1 P2 P3 = (ex4_4 ? ? ? ? P0 P1 P2 P3). -(* multiple inductive existental quantifier (4, 5) *) +(* multiple existental quantifier (4, 5) *) inductive ex4_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3:A0→A1→A2→A3→A4→Prop) : Prop ≝ | ex4_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → ex4_5 ? ? ? ? ? ? ? ? ? . -interpretation "multiple inductive existental quantifier (4, 5)" 'Ex P0 P1 P2 P3 = (ex4_5 ? ? ? ? ? P0 P1 P2 P3). +interpretation "multiple existental quantifier (4, 5)" 'Ex P0 P1 P2 P3 = (ex4_5 ? ? ? ? ? P0 P1 P2 P3). -(* multiple inductive existental quantifier (5, 2) *) +(* multiple existental quantifier (5, 2) *) inductive ex5_2 (A0,A1:Type[0]) (P0,P1,P2,P3,P4:A0→A1→Prop) : Prop ≝ | ex5_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → P2 x0 x1 → P3 x0 x1 → P4 x0 x1 → ex5_2 ? ? ? ? ? ? ? . -interpretation "multiple inductive existental quantifier (5, 2)" 'Ex P0 P1 P2 P3 P4 = (ex5_2 ? ? P0 P1 P2 P3 P4). +interpretation "multiple existental quantifier (5, 2)" 'Ex P0 P1 P2 P3 P4 = (ex5_2 ? ? P0 P1 P2 P3 P4). -(* multiple inductive existental quantifier (5, 3) *) +(* multiple existental quantifier (5, 3) *) inductive ex5_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→Prop) : Prop ≝ | ex5_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → P4 x0 x1 x2 → ex5_3 ? ? ? ? ? ? ? ? . -interpretation "multiple inductive existental quantifier (5, 3)" 'Ex P0 P1 P2 P3 P4 = (ex5_3 ? ? ? P0 P1 P2 P3 P4). +interpretation "multiple existental quantifier (5, 3)" 'Ex P0 P1 P2 P3 P4 = (ex5_3 ? ? ? P0 P1 P2 P3 P4). -(* multiple inductive existental quantifier (5, 4) *) +(* multiple existental quantifier (5, 4) *) inductive ex5_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→A3→Prop) : Prop ≝ | ex5_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → ex5_4 ? ? ? ? ? ? ? ? ? . -interpretation "multiple inductive existental quantifier (5, 4)" 'Ex P0 P1 P2 P3 P4 = (ex5_4 ? ? ? ? P0 P1 P2 P3 P4). +interpretation "multiple existental quantifier (5, 4)" 'Ex P0 P1 P2 P3 P4 = (ex5_4 ? ? ? ? P0 P1 P2 P3 P4). -(* multiple inductive existental quantifier (5, 5) *) +(* multiple existental quantifier (5, 5) *) inductive ex5_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→A3→A4→Prop) : Prop ≝ | ex5_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → P4 x0 x1 x2 x3 x4 → ex5_5 ? ? ? ? ? ? ? ? ? ? . -interpretation "multiple inductive existental quantifier (5, 5)" 'Ex P0 P1 P2 P3 P4 = (ex5_5 ? ? ? ? ? P0 P1 P2 P3 P4). +interpretation "multiple existental quantifier (5, 5)" 'Ex P0 P1 P2 P3 P4 = (ex5_5 ? ? ? ? ? P0 P1 P2 P3 P4). -(* multiple inductive existental quantifier (5, 6) *) +(* multiple existental quantifier (5, 6) *) inductive ex5_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→A3→A4→A5→Prop) : Prop ≝ | ex5_6_intro: ∀x0,x1,x2,x3,x4,x5. P0 x0 x1 x2 x3 x4 x5 → P1 x0 x1 x2 x3 x4 x5 → P2 x0 x1 x2 x3 x4 x5 → P3 x0 x1 x2 x3 x4 x5 → P4 x0 x1 x2 x3 x4 x5 → ex5_6 ? ? ? ? ? ? ? ? ? ? ? . -interpretation "multiple inductive existental quantifier (5, 6)" 'Ex P0 P1 P2 P3 P4 = (ex5_6 ? ? ? ? ? ? P0 P1 P2 P3 P4). +interpretation "multiple existental quantifier (5, 6)" 'Ex P0 P1 P2 P3 P4 = (ex5_6 ? ? ? ? ? ? P0 P1 P2 P3 P4). -(* multiple inductive existental quantifier (6, 3) *) +(* multiple existental quantifier (6, 3) *) inductive ex6_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→Prop) : Prop ≝ | ex6_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → P4 x0 x1 x2 → P5 x0 x1 x2 → ex6_3 ? ? ? ? ? ? ? ? ? . -interpretation "multiple inductive existental quantifier (6, 3)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_3 ? ? ? P0 P1 P2 P3 P4 P5). +interpretation "multiple existental quantifier (6, 3)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_3 ? ? ? P0 P1 P2 P3 P4 P5). -(* multiple inductive existental quantifier (6, 4) *) +(* multiple existental quantifier (6, 4) *) inductive ex6_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→Prop) : Prop ≝ | ex6_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → P5 x0 x1 x2 x3 → ex6_4 ? ? ? ? ? ? ? ? ? ? . -interpretation "multiple inductive existental quantifier (6, 4)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_4 ? ? ? ? P0 P1 P2 P3 P4 P5). +interpretation "multiple existental quantifier (6, 4)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_4 ? ? ? ? P0 P1 P2 P3 P4 P5). -(* multiple inductive existental quantifier (6, 5) *) +(* multiple existental quantifier (6, 5) *) inductive ex6_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→A4→Prop) : Prop ≝ | ex6_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → P4 x0 x1 x2 x3 x4 → P5 x0 x1 x2 x3 x4 → ex6_5 ? ? ? ? ? ? ? ? ? ? ? . -interpretation "multiple inductive existental quantifier (6, 5)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_5 ? ? ? ? ? P0 P1 P2 P3 P4 P5). +interpretation "multiple existental quantifier (6, 5)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_5 ? ? ? ? ? P0 P1 P2 P3 P4 P5). -(* multiple inductive existental quantifier (6, 6) *) +(* multiple existental quantifier (6, 6) *) inductive ex6_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→A4→A5→Prop) : Prop ≝ | ex6_6_intro: ∀x0,x1,x2,x3,x4,x5. P0 x0 x1 x2 x3 x4 x5 → P1 x0 x1 x2 x3 x4 x5 → P2 x0 x1 x2 x3 x4 x5 → P3 x0 x1 x2 x3 x4 x5 → P4 x0 x1 x2 x3 x4 x5 → P5 x0 x1 x2 x3 x4 x5 → ex6_6 ? ? ? ? ? ? ? ? ? ? ? ? . -interpretation "multiple inductive existental quantifier (6, 6)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_6 ? ? ? ? ? ? P0 P1 P2 P3 P4 P5). +interpretation "multiple existental quantifier (6, 6)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_6 ? ? ? ? ? ? P0 P1 P2 P3 P4 P5). -(* multiple inductive existental quantifier (6, 7) *) +(* multiple existental quantifier (6, 7) *) inductive ex6_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→A4→A5→A6→Prop) : Prop ≝ | ex6_7_intro: ∀x0,x1,x2,x3,x4,x5,x6. P0 x0 x1 x2 x3 x4 x5 x6 → P1 x0 x1 x2 x3 x4 x5 x6 → P2 x0 x1 x2 x3 x4 x5 x6 → P3 x0 x1 x2 x3 x4 x5 x6 → P4 x0 x1 x2 x3 x4 x5 x6 → P5 x0 x1 x2 x3 x4 x5 x6 → ex6_7 ? ? ? ? ? ? ? ? ? ? ? ? ? . -interpretation "multiple inductive existental quantifier (6, 7)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5). +interpretation "multiple existental quantifier (6, 7)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5). -(* multiple inductive existental quantifier (7, 3) *) +(* 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 ? ? ? ? ? ? ? ? ? ? . -interpretation "multiple inductive existental quantifier (7, 3)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_3 ? ? ? P0 P1 P2 P3 P4 P5 P6). +interpretation "multiple existental quantifier (7, 3)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_3 ? ? ? P0 P1 P2 P3 P4 P5 P6). -(* multiple inductive existental quantifier (7, 4) *) +(* multiple existental quantifier (7, 4) *) inductive ex7_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→Prop) : Prop ≝ | ex7_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → P5 x0 x1 x2 x3 → P6 x0 x1 x2 x3 → ex7_4 ? ? ? ? ? ? ? ? ? ? ? . -interpretation "multiple inductive existental quantifier (7, 4)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6). +interpretation "multiple existental quantifier (7, 4)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6). -(* multiple inductive existental quantifier (7, 7) *) +(* multiple existental quantifier (7, 7) *) inductive ex7_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→A5→A6→Prop) : Prop ≝ | ex7_7_intro: ∀x0,x1,x2,x3,x4,x5,x6. P0 x0 x1 x2 x3 x4 x5 x6 → P1 x0 x1 x2 x3 x4 x5 x6 → P2 x0 x1 x2 x3 x4 x5 x6 → P3 x0 x1 x2 x3 x4 x5 x6 → P4 x0 x1 x2 x3 x4 x5 x6 → P5 x0 x1 x2 x3 x4 x5 x6 → P6 x0 x1 x2 x3 x4 x5 x6 → ex7_7 ? ? ? ? ? ? ? ? ? ? ? ? ? ? . -interpretation "multiple inductive existental quantifier (7, 7)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6). +interpretation "multiple existental quantifier (7, 7)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6). -(* multiple inductive existental quantifier (8, 4) *) +(* 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 ? ? ? ? ? ? ? ? ? ? ? ? . -interpretation "multiple inductive existental quantifier (8, 4)" 'Ex P0 P1 P2 P3 P4 P5 P6 P7 = (ex8_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6 P7). +interpretation "multiple existental quantifier (8, 4)" 'Ex P0 P1 P2 P3 P4 P5 P6 P7 = (ex8_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6 P7). -(* multiple inductive existental quantifier (8, 5) *) +(* multiple existental quantifier (8, 5) *) inductive ex8_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3,P4,P5,P6,P7:A0→A1→A2→A3→A4→Prop) : Prop ≝ | ex8_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → P4 x0 x1 x2 x3 x4 → P5 x0 x1 x2 x3 x4 → P6 x0 x1 x2 x3 x4 → P7 x0 x1 x2 x3 x4 → ex8_5 ? ? ? ? ? ? ? ? ? ? ? ? ? . -interpretation "multiple inductive existental quantifier (8, 5)" 'Ex P0 P1 P2 P3 P4 P5 P6 P7 = (ex8_5 ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6 P7). +interpretation "multiple existental quantifier (8, 5)" 'Ex P0 P1 P2 P3 P4 P5 P6 P7 = (ex8_5 ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6 P7). (* multiple disjunction connective (3) *) -- 2.39.2