]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/dtd/provastruct.theory.xml
projects / helm.git / blobdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | inline | side by side
Initial revision
[helm.git] / helm / dtd / provastruct.theory.xml
diff --git a/helm/dtd/provastruct.theory.xml b/helm/dtd/provastruct.theory.xml
new file mode 100644 (file)
index 0000000..23c8f7c
--- /dev/null
+++ b/helm/dtd/provastruct.theory.xml
@@ -0,0 +1,158 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE SECTION SYSTEM "theoryobject.dtd">
+
+<SECTION>
+ 
+ <SECTION>
+  <Variable name="A" xmlns:m="http://www.w3.org/1998/Math/MathML"><type>
+    <m:math><m:apply><m:csymbol>cast</m:csymbol>
+      
+        <m:apply><m:csymbol>Prop</m:csymbol></m:apply>
+      
+      
+        <m:apply><m:csymbol>Type</m:csymbol></m:apply>
+      
+    </m:apply></m:math>
+  </type></Variable>
+  <SECTION>
+   <Variable name="B" xmlns:m="http://www.w3.org/1998/Math/MathML"><type>
+    <m:math><m:apply><m:csymbol>cast</m:csymbol>
+      
+        <m:apply><m:csymbol>Prop</m:csymbol></m:apply>
+      
+      
+        <m:apply><m:csymbol>Type</m:csymbol></m:apply>
+      
+    </m:apply></m:math>
+  </type></Variable>
+   <Axiom name="axiom" xmlns:m="http://www.w3.org/1998/Math/MathML"><Params>1: A 0: B</Params><type>
+    <m:math><m:apply><m:csymbol>cast</m:csymbol>
+      
+        <m:apply><m:csymbol>arrow</m:csymbol>
+            <m:ci>A</m:ci>
+          
+            <m:apply><m:csymbol>arrow</m:csymbol>
+                <m:apply><m:csymbol>arrow</m:csymbol>
+                    <m:ci>A</m:ci>
+                  
+                    <m:ci>B</m:ci>
+                  </m:apply>
+              
+                <m:ci>B</m:ci>
+              </m:apply>
+          </m:apply>
+      
+      
+        <m:apply><m:csymbol>Prop</m:csymbol></m:apply>
+      
+    </m:apply></m:math>
+  </type></Axiom>
+   <Definition name="th1" xmlns:m="http://www.w3.org/1998/Math/MathML"><Params>1: A 0: B</Params><body>
+    <m:math><m:lambda><m:bvar><m:ci>A0</m:ci><m:type>
+        <m:ci>A</m:ci>
+      </m:type></m:bvar>
+        <m:lambda><m:bvar><m:ci>H</m:ci><m:type>
+            <m:apply><m:csymbol>arrow</m:csymbol>
+                <m:ci>A</m:ci>
+              
+                <m:ci>B</m:ci>
+              </m:apply>
+          </m:type></m:bvar>
+            <m:apply><m:csymbol>app</m:csymbol>
+              <m:ci definitionURL="cic:/coq/INIT/Logic/Conjunction/and.ind">conj</m:ci>
+              <m:ci>A</m:ci>
+              <m:ci>B</m:ci>
+              <m:ci>A0</m:ci>
+              <m:apply><m:csymbol>app</m:csymbol>
+                <m:ci definitionURL="cic:/prove/provastruct/a/b1/axiom.con">axiom</m:ci>
+                <m:ci>A0</m:ci>
+                <m:ci>H</m:ci>
+              </m:apply>
+            </m:apply>
+          </m:lambda>
+      </m:lambda></m:math>
+  </body><type>
+    <m:math><m:apply><m:csymbol>cast</m:csymbol>
+      
+        <m:apply><m:csymbol>arrow</m:csymbol>
+            <m:ci>A</m:ci>
+          
+            <m:apply><m:csymbol>arrow</m:csymbol>
+                <m:apply><m:csymbol>arrow</m:csymbol>
+                    <m:ci>A</m:ci>
+                  
+                    <m:ci>B</m:ci>
+                  </m:apply>
+              
+                <m:apply><m:and definitionURL="cic:/coq/INIT/Logic/Conjunction/and.ind"/><m:ci>A</m:ci><m:ci>B</m:ci></m:apply>
+              </m:apply>
+          </m:apply>
+      
+      
+        <m:apply><m:csymbol>Prop</m:csymbol></m:apply>
+      
+    </m:apply></m:math>
+  </type></Definition>
+  </SECTION>
+  <SECTION>
+   <Variable name="B" xmlns:m="http://www.w3.org/1998/Math/MathML"><type>
+    <m:math><m:apply><m:csymbol>cast</m:csymbol>
+      
+        <m:apply><m:csymbol>Set</m:csymbol></m:apply>
+      
+      
+        <m:apply><m:csymbol>Type</m:csymbol></m:apply>
+      
+    </m:apply></m:math>
+  </type></Variable>
+   <Axiom name="axiom&apos;" xmlns:m="http://www.w3.org/1998/Math/MathML"><Params>1: A</Params><type>
+    <m:math><m:apply><m:csymbol>cast</m:csymbol>
+      
+        <m:apply><m:csymbol>prod</m:csymbol><m:bvar><m:ci>A</m:ci><m:type>
+            <m:apply><m:csymbol>Prop</m:csymbol></m:apply>
+          </m:type></m:bvar>
+            <m:apply><m:csymbol>arrow</m:csymbol>
+                <m:ci>A</m:ci>
+              
+                <m:ci>A</m:ci>
+              </m:apply>
+          </m:apply>
+      
+      
+        <m:apply><m:csymbol>Prop</m:csymbol></m:apply>
+      
+    </m:apply></m:math>
+  </type></Axiom>
+  </SECTION>
+  <Definition name="th1&apos;" xmlns:m="http://www.w3.org/1998/Math/MathML"><Params>0: A</Params><body>
+    <m:math><m:lambda><m:bvar><m:ci>A0</m:ci><m:type>
+        <m:apply><m:csymbol>Prop</m:csymbol></m:apply>
+      </m:type></m:bvar>
+        <m:lambda><m:bvar><m:ci>H</m:ci><m:type>
+            <m:ci>A0</m:ci>
+          </m:type></m:bvar>
+            <m:ci>H</m:ci>
+          </m:lambda>
+      </m:lambda></m:math>
+  </body><type>
+    <m:math><m:apply><m:csymbol>cast</m:csymbol>
+      
+        <m:apply><m:csymbol>prod</m:csymbol><m:bvar><m:ci>A</m:ci><m:type>
+            <m:apply><m:csymbol>Prop</m:csymbol></m:apply>
+          </m:type></m:bvar>
+            <m:apply><m:csymbol>arrow</m:csymbol>
+                <m:ci>A</m:ci>
+              
+                <m:ci>A</m:ci>
+              </m:apply>
+          </m:apply>
+      
+      
+        <m:apply><m:csymbol>Prop</m:csymbol></m:apply>
+      
+    </m:apply></m:math>
+  </type></Definition>
+ </SECTION>
+</SECTION>
+
+<!-- This page was served in 4037 milliseconds by Cocoon 1.7.3 -->
Unnamed repository; edit this file 'description' to name the repository.