X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FDEVEL%2Fmlminidom%2Ftest.xml;fp=helm%2FDEVEL%2Fmlminidom%2Ftest.xml;h=83d2eef68bbdf76d2246b7993d56678810452f8d;hb=d70d5de1ec9ccc86c9df45036245af34c37575ea;hp=0000000000000000000000000000000000000000;hpb=99d60351f793983bb7633334ea59e95feb36c72c;p=helm.git diff --git a/helm/DEVEL/mlminidom/test.xml b/helm/DEVEL/mlminidom/test.xml new file mode 100644 index 000000000..83d2eef68 --- /dev/null +++ b/helm/DEVEL/mlminidom/test.xml @@ -0,0 +1,505 @@ + + + + + + + + DEFINITION and_ind() OF TYPE + + + + + + + + __ + + + + + + + + ( + + + + + Π + A + : + + Prop + + + + + + + . + + + + + Π + B + : + + Prop + + + + + + + . + + + + + Π + P + : + + Prop + + + + + + + . + + + + + Π + f + : + + ( + A + → + + ( + B + → + P + ) + + ) + + + + + + + . + + Π + a + : + + ( + and + + _ + + A + + _ + + B + ) + + . + P + + + + + + + + + + + + + + + + + + + + + + + + + + + + :> + + Prop + + + + + + + + ) + + + + + + + + cast + + prod + + A + + + Prop + + + + + prod + + B + + + Prop + + + + + prod + + P + + + Prop + + + + + prod + + f + + + arrow + A + + arrow + B + P + + + + + + prod + + a + + + app + and + A + B + + + + P + + + + + + + Prop + + + + + + + + + + + AS + + + + + + + + __ + + + + + + + λ + A + : + + Prop + + + + + + + . + + + + + λ + B + : + + Prop + + + + + + + . + + + + + λ + P + : + + Prop + + + + + + + . + + + + + λ + f + : + + ( + A + → + + ( + B + → + P + ) + + ) + + + + + + + . + + + + + λ + a + : + + ( + and + + _ + + A + + _ + + B + ) + + + + + + + . + + < + P + > + CASES + + _ + + a + + _ + + OF + + ( + conj + + _ + + $1 + + _ + + $2 + ) + + ⇒ + + ( + f + + _ + + $1 + + _ + + $2 + ) + + + _ + + END + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + A + + + Prop + + + + + + B + + + Prop + + + + + + P + + + Prop + + + + + + f + + + arrow + A + + arrow + B + P + + + + + + + a + + + app + and + A + B + + + + + mutcase + P + a + + app + conj + $1 + $2 + + + app + f + $1 + $2 + + + + + + + + + + + + + +