helm/dtd/provastruct.theory.xml

   1 <?xml version="1.0" encoding="UTF-8"?>
   2 <!DOCTYPE SECTION SYSTEM "theoryobject.dtd">
   3
   4 <SECTION>
   5
   6  <SECTION>
   7   <Variable name="A" xmlns:m="http://www.w3.org/1998/Math/MathML"><type>
   8     <m:math><m:apply><m:csymbol>cast</m:csymbol>
   9
  10         <m:apply><m:csymbol>Prop</m:csymbol></m:apply>
  11
  12
  13         <m:apply><m:csymbol>Type</m:csymbol></m:apply>
  14
  15     </m:apply></m:math>
  16   </type></Variable>
  17   <SECTION>
  18    <Variable name="B" xmlns:m="http://www.w3.org/1998/Math/MathML"><type>
  19     <m:math><m:apply><m:csymbol>cast</m:csymbol>
  20
  21         <m:apply><m:csymbol>Prop</m:csymbol></m:apply>
  22
  23
  24         <m:apply><m:csymbol>Type</m:csymbol></m:apply>
  25
  26     </m:apply></m:math>
  27   </type></Variable>
  28    <Axiom name="axiom" xmlns:m="http://www.w3.org/1998/Math/MathML"><Params>1: A 0: B</Params><type>
  29     <m:math><m:apply><m:csymbol>cast</m:csymbol>
  30
  31         <m:apply><m:csymbol>arrow</m:csymbol>
  32             <m:ci>A</m:ci>
  33
  34             <m:apply><m:csymbol>arrow</m:csymbol>
  35                 <m:apply><m:csymbol>arrow</m:csymbol>
  36                     <m:ci>A</m:ci>
  37
  38                     <m:ci>B</m:ci>
  39                   </m:apply>
  40
  41                 <m:ci>B</m:ci>
  42               </m:apply>
  43           </m:apply>
  44
  45
  46         <m:apply><m:csymbol>Prop</m:csymbol></m:apply>
  47
  48     </m:apply></m:math>
  49   </type></Axiom>
  50    <Definition name="th1" xmlns:m="http://www.w3.org/1998/Math/MathML"><Params>1: A 0: B</Params><body>
  51     <m:math><m:lambda><m:bvar><m:ci>A0</m:ci><m:type>
  52         <m:ci>A</m:ci>
  53       </m:type></m:bvar>
  54         <m:lambda><m:bvar><m:ci>H</m:ci><m:type>
  55             <m:apply><m:csymbol>arrow</m:csymbol>
  56                 <m:ci>A</m:ci>
  57
  58                 <m:ci>B</m:ci>
  59               </m:apply>
  60           </m:type></m:bvar>
  61             <m:apply><m:csymbol>app</m:csymbol>
  62               <m:ci definitionURL="cic:/coq/INIT/Logic/Conjunction/and.ind">conj</m:ci>
  63               <m:ci>A</m:ci>
  64               <m:ci>B</m:ci>
  65               <m:ci>A0</m:ci>
  66               <m:apply><m:csymbol>app</m:csymbol>
  67                 <m:ci definitionURL="cic:/prove/provastruct/a/b1/axiom.con">axiom</m:ci>
  68                 <m:ci>A0</m:ci>
  69                 <m:ci>H</m:ci>
  70               </m:apply>
  71             </m:apply>
  72           </m:lambda>
  73       </m:lambda></m:math>
  74   </body><type>
  75     <m:math><m:apply><m:csymbol>cast</m:csymbol>
  76
  77         <m:apply><m:csymbol>arrow</m:csymbol>
  78             <m:ci>A</m:ci>
  79
  80             <m:apply><m:csymbol>arrow</m:csymbol>
  81                 <m:apply><m:csymbol>arrow</m:csymbol>
  82                     <m:ci>A</m:ci>
  83
  84                     <m:ci>B</m:ci>
  85                   </m:apply>
  86
  87                 <m:apply><m:and definitionURL="cic:/coq/INIT/Logic/Conjunction/and.ind"/><m:ci>A</m:ci><m:ci>B</m:ci></m:apply>
  88               </m:apply>
  89           </m:apply>
  90
  91
  92         <m:apply><m:csymbol>Prop</m:csymbol></m:apply>
  93
  94     </m:apply></m:math>
  95   </type></Definition>
  96   </SECTION>
  97   <SECTION>
  98    <Variable name="B" xmlns:m="http://www.w3.org/1998/Math/MathML"><type>
  99     <m:math><m:apply><m:csymbol>cast</m:csymbol>
 100
 101         <m:apply><m:csymbol>Set</m:csymbol></m:apply>
 102
 103
 104         <m:apply><m:csymbol>Type</m:csymbol></m:apply>
 105
 106     </m:apply></m:math>
 107   </type></Variable>
 108    <Axiom name="axiom&apos;" xmlns:m="http://www.w3.org/1998/Math/MathML"><Params>1: A</Params><type>
 109     <m:math><m:apply><m:csymbol>cast</m:csymbol>
 110
 111         <m:apply><m:csymbol>prod</m:csymbol><m:bvar><m:ci>A</m:ci><m:type>
 112             <m:apply><m:csymbol>Prop</m:csymbol></m:apply>
 113           </m:type></m:bvar>
 114             <m:apply><m:csymbol>arrow</m:csymbol>
 115                 <m:ci>A</m:ci>
 116
 117                 <m:ci>A</m:ci>
 118               </m:apply>
 119           </m:apply>
 120
 121
 122         <m:apply><m:csymbol>Prop</m:csymbol></m:apply>
 123
 124     </m:apply></m:math>
 125   </type></Axiom>
 126   </SECTION>
 127   <Definition name="th1&apos;" xmlns:m="http://www.w3.org/1998/Math/MathML"><Params>0: A</Params><body>
 128     <m:math><m:lambda><m:bvar><m:ci>A0</m:ci><m:type>
 129         <m:apply><m:csymbol>Prop</m:csymbol></m:apply>
 130       </m:type></m:bvar>
 131         <m:lambda><m:bvar><m:ci>H</m:ci><m:type>
 132             <m:ci>A0</m:ci>
 133           </m:type></m:bvar>
 134             <m:ci>H</m:ci>
 135           </m:lambda>
 136       </m:lambda></m:math>
 137   </body><type>
 138     <m:math><m:apply><m:csymbol>cast</m:csymbol>
 139
 140         <m:apply><m:csymbol>prod</m:csymbol><m:bvar><m:ci>A</m:ci><m:type>
 141             <m:apply><m:csymbol>Prop</m:csymbol></m:apply>
 142           </m:type></m:bvar>
 143             <m:apply><m:csymbol>arrow</m:csymbol>
 144                 <m:ci>A</m:ci>
 145
 146                 <m:ci>A</m:ci>
 147               </m:apply>
 148           </m:apply>
 149
 150
 151         <m:apply><m:csymbol>Prop</m:csymbol></m:apply>
 152
 153     </m:apply></m:math>
 154   </type></Definition>
 155  </SECTION>
 156 </SECTION>
 157
 158 <!-- This page was served in 4037 milliseconds by Cocoon 1.7.3 -->