helm/papers/calculemus-2003/slides/misc/startmusing.xml

   1 <?xml version="1.0"?>
   2 <start_musing id="X;h9@Xgt=sT|HF7owBaa+h,c[DbU5-b0"><gTopLevelStatus>
   3 <CurrentGoal>2</CurrentGoal>
   4 <ConstantType id="1" name="dummy" params="">
   5   <PROD type="Prop">
   6     <decl binder="x" id="i164" type="Type">
   7       <CONST id="i262" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R.con"/>
   8     </decl>
   9     <target>
  10       <APPLY id="i166" sort="Type">
  11         <MUTIND id="i168" noType="0" uri="cic:/Coq/Init/Logic_Type/eqT.ind"/>
  12         <CONST id="i176" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R.con"/>
  13         <REL binder="x" id="i178" idref="i164" sort="Type" value="1"/>
  14         <APPLY id="i180" sort="Type">
  15           <CONST id="i182" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rdiv.con"/>
  16           <APPLY id="i188" sort="Type">
  17             <CONST id="i190" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rminus.con"/>
  18             <APPLY id="i196" sort="Type">
  19               <CONST id="i198" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rminus.con"/>
  20               <APPLY id="i204" sort="Type">
  21                 <CONST id="i206" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rmult.con"/>
  22                 <APPLY id="i212" sort="Type">
  23                   <CONST id="i214" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rplus.con"/>
  24                   <REL binder="x" id="i220" idref="i164" sort="Type" value="1"/>
  25                   <CONST id="i222" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
  26                 </APPLY>
  27                 <APPLY id="i224" sort="Type">
  28                   <CONST id="i226" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rplus.con"/>
  29                   <REL binder="x" id="i232" idref="i164" sort="Type" value="1"/>
  30                   <CONST id="i234" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
  31                 </APPLY>
  32               </APPLY>
  33               <CONST id="i236" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
  34             </APPLY>
  35             <APPLY id="i238" sort="Type">
  36               <CONST id="i240" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rmult.con"/>
  37               <REL binder="x" id="i246" idref="i164" sort="Type" value="1"/>
  38               <REL binder="x" id="i248" idref="i164" sort="Type" value="1"/>
  39             </APPLY>
  40           </APPLY>
  41           <APPLY id="i250" sort="Type">
  42             <CONST id="i252" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rplus.con"/>
  43             <CONST id="i258" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
  44             <CONST id="i260" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
  45           </APPLY>
  46         </APPLY>
  47       </APPLY>
  48     </target>
  49   </PROD>
  50 </ConstantType>
  51 <CurrentProof id="1" of="cic:/dummy.con">
  52   <Conjecture id="c0" no="2">
  53     <Decl id="h0" name="x">
  54       <CONST id="i0" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R.con"/>
  55     </Decl>
  56     <Goal>
  57       <APPLY id="i2" sort="Type">
  58         <MUTIND id="i4" noType="0" uri="cic:/Coq/Init/Logic_Type/eqT.ind"/>
  59         <CONST id="i12" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R.con"/>
  60         <REL binder="x" id="i14" idref="h0" sort="Type" value="1"/>
  61         <APPLY id="i16" sort="Type">
  62           <CONST id="i18" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rdiv.con"/>
  63           <APPLY id="i24" sort="Type">
  64             <CONST id="i26" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rminus.con"/>
  65             <APPLY id="i32" sort="Type">
  66               <CONST id="i34" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rminus.con"/>
  67               <APPLY id="i40" sort="Type">
  68                 <CONST id="i42" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rmult.con"/>
  69                 <APPLY id="i48" sort="Type">
  70                   <CONST id="i50" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rplus.con"/>
  71                   <REL binder="x" id="i56" idref="h0" sort="Type" value="1"/>
  72                   <CONST id="i58" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
  73                 </APPLY>
  74                 <APPLY id="i60" sort="Type">
  75                   <CONST id="i62" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rplus.con"/>
  76                   <REL binder="x" id="i68" idref="h0" sort="Type" value="1"/>
  77                   <CONST id="i70" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
  78                 </APPLY>
  79               </APPLY>
  80               <CONST id="i72" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
  81             </APPLY>
  82             <APPLY id="i74" sort="Type">
  83               <CONST id="i76" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rmult.con"/>
  84               <REL binder="x" id="i82" idref="h0" sort="Type" value="1"/>
  85               <REL binder="x" id="i84" idref="h0" sort="Type" value="1"/>
  86             </APPLY>
  87           </APPLY>
  88           <APPLY id="i86" sort="Type">
  89             <CONST id="i88" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rplus.con"/>
  90             <CONST id="i94" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
  91             <CONST id="i96" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
  92           </APPLY>
  93         </APPLY>
  94       </APPLY>
  95     </Goal>
  96   </Conjecture>
  97   <body>
  98     <LAMBDA sort="Prop">
  99       <decl binder="x" id="i98" type="Type">
 100         <CONST id="i162" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R.con"/>
 101       </decl>
 102       <target>
 103         <META id="i130" no="2" sort="Prop">
 104           <substitution>
 105             <REL binder="x" id="i160" idref="i98" sort="Type" value="1"/>
 106           </substitution>
 107         </META>
 108       </target>
 109     </LAMBDA>
 110   </body>
 111 </CurrentProof>
 112 </gTopLevelStatus>
 113 </start_musing>