- matex: we separate axioms (propositions) and assumptions (other)

[helm.git] / matita / components / binaries / matex / test / basic_1.sty

diff --git a/matita/components/binaries/matex/test/basic_1.sty b/matita/components/binaries/matex/test/basic_1.sty
index 27fbe98b29370931511c09205003976f53224640..71e48ff0235dcb3606f19b036d708011065573bd 100644 (file)
--- a/matita/components/binaries/matex/test/basic_1.sty
+++ b/matita/components/binaries/matex/test/basic_1.sty
@@ -1,5 +1,5 @@
 \NeedsTeXFormat{LaTeX2e}[1995/12/01]
-\ProvidesPackage{basic_1}[2016/06/24 Notation for "cic:/matita/lambdadelta/basic_1/"]
+\ProvidesPackage{basic_1}[2016/07/03 Notation for "cic:/matita/lambdadelta/basic_1/"]
 \RequirePackage{legacy_1}
 \RequirePackage{ground_1}
 \ExecuteOptions{}
@@ -14,19 +14,25 @@
 \newcommand*\ld@oB[1]{\mathopen{\lBrack}}
 \newcommand*\ld@cB[1]{\mathopen{\rBrack}}
 \newcommand*\ld@env[1]{\mathrel{\vdash}}
+\newcommand*\ld@fs[1]{\mathord{.}}
 
+\newcommand*\ld@appl[1]{\setbinlink{@}{#1}{}}
+\newcommand*\ld@appls[1]{\setbinlink{\overline{@}}{#1}{}}
 \newcommand*\ld@arity[2]{\setrellink{\mathsf{arity}}{#1}{#2}}
+\newcommand*\ld@bind[1]{\setordlink{\mathbf{B}}{#1}{}}
 \newcommand*\ld@coconverts[1]{\setrellink{\mathsf{convert}_{\mathord\oplusrhrim}^*}{#1}{}}
-\newcommand*\ld@convert[1]{\setrellink{\mathsf{convert}}{#1}{}}
 \newcommand*\ld@converts[1]{\setrellink{\mathsf{convert}^*}{#1}{}}
+\newcommand*\ld@copremise[2]{\setoplink{\mathsf{copremise}}{#1}{#2}}
 \newcommand*\ld@coweight[1]{\setoplink{\equivVvert}{#1}{}}
 \newcommand*\ld@drop[2]{\setoplink{\Downarrow}{#1}{#2}}
 \newcommand*\ld@drops[2]{\setoplink{\Downarrow^*}{#1}{#2}}
 \newcommand*\ld@equiv[2]{\setrellink{\equiv}{#1}{#2}}
+\newcommand*\ld@flat[1]{\setoplink{\mathbf{F}}{#1}{}}
 \newcommand*\ld@funlift[2]{\setoplink{\uparrow}{#1}{#2}}
-\newcommand*\ld@funlifts[2]{\setoplink{\uparrow^*}{#1}{}}
+\newcommand*\ld@funlifts[2]{\setoplink{\uparrow^*}{#1}{#2}}
 \newcommand*\ld@funv[2]{\setoplink{\mathsf{v}}{#1}{#2}}
 \newcommand*\ld@funw[2]{\setoplink{\mathsf{w}}{#1}{#2}}
+\newcommand*\ld@pair[2]{\setordlink{\mathbf{P}}{#1}{#2}}
 \newcommand*\ld@in[1]{\setrellink{\in}{#1}{}}
 \newcommand*\ld@leaf[1]{\setoplink{\star}{#1}{}}
 \newcommand*\ld@length@open[1]{\setopenlink{\vert}{#1}}
@@ -34,6 +40,10 @@
 \newcommand*\ld@lenv[1]{\setoplink{\mathsf{lenv}}{#1}{}}
 \newcommand*\ld@level[1]{\setoplink{\mathsf{level}}{#1}{}}
 \newcommand*\ld@lref[1]{\setoplink{\#}{#1}{}}
+\newcommand*\ld@lsup[2]{\setrellink{\sqsupseteq}{#1}{#2}}
+\newcommand*\ld@lsupa[2]{\setrellink{\mathord\sqsupseteq\lozenge}{#1}{#2}}
+\newcommand*\ld@lsupt[2]{\setrellink{\mathord\sqsupseteq\mathord:}{#1}{#2}}
+\newcommand*\ld@mksh[1]{\setordlink{\mathbf{H}}{#1}{}}
 \newcommand*\ld@next[2]{\setoplink{\mathsf{next}}{#1}{#2}}
 \newcommand*\ld@rcandidate[2]{\setoplink{\mathsf{r\_candidate}}{#1}{#2}}
 \newcommand*\ld@rnormal[1]{\setoplink{\mathsf{r\_normal}}{#1}{}}
@@ -42,6 +52,7 @@
 \newcommand*\ld@rstrong[1]{\setoplink{\mathsf{r\_strong}}{#1}{}}
 \newcommand*\ld@sametop[1]{\setrellink{\eqsim}{#1}{}}
 \newcommand*\ld@shift[1]{\setordlink{.}{#1}}
+\newcommand*\ld@subeq[1]{\setrellink{\subseteq}{#1}{}}
 \newcommand*\ld@subst[1]{\setbinlink{/}{#1}{}}
 \newcommand*\ld@substs[1]{\setbinlink{/^*}{#1}{}}
 \newcommand*\ld@to[1]{\setrellink{\rightarrow}{#1}{}}
@@ -53,14 +64,18 @@
 
 \newcommand*\ld@tuple@a[2]{\ld@oa{#1}#2\ld@ca{#1}}
 
+\newcommand*\Appl[3]{#2\ld@appl{#1}#3}
+\newcommand*\ApplS[3]{#2\ld@appls{#1}#3}
 \newcommand*\Arity[5]{#3\ld@env{#1}#4\ld@arity{#1}{\ld@tuple@a{#1}{#2}}#5}
 \newcommand*\AtomA[2]{\ld@leaf{#1}#2}
 \newcommand*\AtomB[3]{\ld@leaf{#1}\ld@tuple@b{#1}{#2}{#3}}
+\newcommand*\Bind[2]{\ld@bind{#1}\ld@tuple@a{#1}{#2}}
 \newcommand*\CoConsA[3]{#2\ld@cocons{#1}#3}
-\newcommand*\CoConvertS[4]{#2\ld@env{#1}#3\ld@coconverts{#1}#4}
+\newcommand*\CoConvertSA[4]{#2\ld@env{#1}#3\ld@coconverts{#1}#4}
 \newcommand*\ConsA[3]{#2\ld@cons{#1}#3}
-\newcommand*\Convert[4]{#2\ld@env{#1}#3\ld@convert{#1}#4}
-\newcommand*\ConvertS[4]{#2\ld@env{#1}#3\ld@converts{#1}#4}
+\newcommand*\ConvertS[3]{#2\ld@converts{#1}#3}
+\newcommand*\ConvertSA[4]{#2\ld@env{#1}#3\ld@converts{#1}#4}
+\newcommand*\CoPremise[4]{\ld@copremise{#1}{\ld@tuple@a{#1}{#2}}#3\ld@eq{#1}#4}
 \newcommand*\CoWeightA[2]{\ld@coweight{#1}\ld@tuple@a{#1}{#2}}
 \newcommand*\CoWeightB[3]{\ld@coweight{#1}\ld@tuple@b{#1}{#2}{#3}}
 \newcommand*\Drop[3]{\ld@drop{#1}{}#2\ld@eq{#1}#3}
@@ -69,6 +84,7 @@
 \newcommand*\DropS[4]{\ld@drops{#1}{\ld@tuple@a{#1}{#2}}#3\ld@eq{#1}#4}
 \renewcommand*\Equiv[3]{#2\ld@equiv{#1}{}#3}
 \newcommand*\EquivA[4]{#3\ld@equiv{#1}{\ld@tuple@a{#1}{#2}}#4}
+\newcommand*\Flat[2]{\ld@flat{#1}\ld@tuple@a{#1}{#2}}
 \newcommand*\FunLift[4]{\ld@funlift{#1}{\ld@tuple@b{#1}{#2}{#3}}#4}
 \newcommand*\FunLiftS[3]{\ld@funlifts{#1}{\ld@tuple@a{#1}{#2}}#3}
 \newcommand*\FunSubstS[4]{\mathop{\ld@ob{#1}#3\ld@substs{#1}#2\ld@cb{#1}}#4}
@@ -77,9 +93,17 @@
 \newcommand*\LEnv[2]{\ld@lenv{#1}#2}
 \newcommand*\Length[2]{\ld@length@open{#1}#2\ld@length@close{#1}}
 \newcommand*\Level[2]{\ld@level{#1}#2}
+\newcommand*\LHead[4]{#2\ld@fs{#1}\ld@pair{#1}{\ld@tuple@a{#1}{#3}}#4}
 \newcommand*\LRef[2]{\ld@lref{#1}#2}
+\newcommand*\LSup[3]{#2\ld@lsup{#1}{}#3}
+\newcommand*\LSupA[4]{#3\ld@lsupa{#1}{\ld@tuple@a{#1}{#2}}#4}
+\newcommand*\LSupC[4]{#3\ld@lsup{#1}{\ld@tuple@a{#1}{#2}}#4}
+\newcommand*\LSupT[4]{#3\ld@lsupt{#1}{\ld@tuple@a{#1}{#2}}#4}
 \newcommand*\LTB[5]{\ld@tuple@b{#1}{#2}{#3}\ld@lt{#1}\ld@tuple@b{#1}{#4}{#5}}
+\newcommand*\MkSH[3]{\ld@mksh{#1}\ld@tuple@b{#1}{#2}{#3}}
 \newcommand*\Next[3]{\ld@next{#1}{\ld@tuple@a{#1}{#2}}#3}
+\newcommand*\NextS[4]{\ld@next{#1}{^{#4}\ld@tuple@a{#1}{#2}}#3}
+\newcommand*\PlusA[4]{#3\ld@plus{#1}{\ld@tuple@a{#1}{#2}}#4}
 \newcommand*\RCandidate[5]{\ld@tuple@b{#1}{#3}{#4}\ld@in{#1}\ld@rcandidate{#1}{\ld@tuple@a{#1}{#2}}#5}
 \newcommand*\RNormal[3]{#2\ld@env{#1}\ld@rnormal{#1}#3}
 \newcommand*\RStep[3]{#2\ld@rstep{#1}#3}
@@ -89,9 +113,12 @@
 \newcommand*\RStrong[3]{#2\ld@env{#1}\ld@rstrong{#1}#3}
 \newcommand*\SameTop[3]{#2\ld@sametop{#1}#3}
 \newcommand*\Shift[3]{#2\ld@shift{#1}#3}
+\newcommand*\SubEq[3]{#2\ld@subeq{#1}#3}
 \newcommand*\Subst[5]{\mathop{\ld@oB{#1}#3\ld@subst{#1}#2\ld@cB{#1}}#4\ld@eq{#1}#5}
 \newcommand*\SubstB[7]{\mathop{\ld@oB{#1}#3\ld@subst{#1}#2\ld@cB{#1}}\ld@tuple@b{#1}{#4}{#5}\ld@eq{#1}\ld@tuple@b{#1}{#6}{#7}}
 \newcommand*\SubstS[5]{\mathop{\ld@oB{#1}#3\ld@substs{#1}#2\ld@cB{#1}}#4\ld@eq{#1}#5}
+\newcommand*\SuccA[3]{\ld@succ{#1}{\ld@tuple@a{#1}{#2}}#3}
+\newcommand*\THead[4]{\ld@pair{#1}{\ld@tuple@a{#1}{#2}}#3\ld@fs{#1}#4}
 \newcommand*\To[3]{#2\ld@to{#1}#3}
 \newcommand*\TStep[5]{#3\ld@env{#1}#4\ld@tstep{#1}{\ld@tuple@a{#1}{#2}}#5}
 \newcommand*\TStepS[5]{#3\ld@env{#1}#4\ld@tsteps{#1}{\ld@tuple@a{#1}{#2}}#5}