talk committed

[helm.git] / helm / papers / calculemus-2003 / slides / misc / startmusing.xml

diff --git a/helm/papers/calculemus-2003/slides/misc/startmusing.xml b/helm/papers/calculemus-2003/slides/misc/startmusing.xml
new file mode 100644 (file)
index 0000000..0f6cd2a
--- /dev/null
+++ b/helm/papers/calculemus-2003/slides/misc/startmusing.xml
@@ -0,0 +1,113 @@
+<?xml version="1.0"?>
+<start_musing id="X;h9@Xgt=sT|HF7owBaa+h,c[DbU5-b0"><gTopLevelStatus>
+<CurrentGoal>2</CurrentGoal>
+<ConstantType id="1" name="dummy" params="">
+  <PROD type="Prop">
+    <decl binder="x" id="i164" type="Type">
+      <CONST id="i262" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R.con"/>
+    </decl>
+    <target>
+      <APPLY id="i166" sort="Type">
+        <MUTIND id="i168" noType="0" uri="cic:/Coq/Init/Logic_Type/eqT.ind"/>
+        <CONST id="i176" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R.con"/>
+        <REL binder="x" id="i178" idref="i164" sort="Type" value="1"/>
+        <APPLY id="i180" sort="Type">
+          <CONST id="i182" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rdiv.con"/>
+          <APPLY id="i188" sort="Type">
+            <CONST id="i190" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rminus.con"/>
+            <APPLY id="i196" sort="Type">
+              <CONST id="i198" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rminus.con"/>
+              <APPLY id="i204" sort="Type">
+                <CONST id="i206" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rmult.con"/>
+                <APPLY id="i212" sort="Type">
+                  <CONST id="i214" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rplus.con"/>
+                  <REL binder="x" id="i220" idref="i164" sort="Type" value="1"/>
+                  <CONST id="i222" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
+                </APPLY>
+                <APPLY id="i224" sort="Type">
+                  <CONST id="i226" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rplus.con"/>
+                  <REL binder="x" id="i232" idref="i164" sort="Type" value="1"/>
+                  <CONST id="i234" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
+                </APPLY>
+              </APPLY>
+              <CONST id="i236" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
+            </APPLY>
+            <APPLY id="i238" sort="Type">
+              <CONST id="i240" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rmult.con"/>
+              <REL binder="x" id="i246" idref="i164" sort="Type" value="1"/>
+              <REL binder="x" id="i248" idref="i164" sort="Type" value="1"/>
+            </APPLY>
+          </APPLY>
+          <APPLY id="i250" sort="Type">
+            <CONST id="i252" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rplus.con"/>
+            <CONST id="i258" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
+            <CONST id="i260" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
+          </APPLY>
+        </APPLY>
+      </APPLY>
+    </target>
+  </PROD>
+</ConstantType>
+<CurrentProof id="1" of="cic:/dummy.con">
+  <Conjecture id="c0" no="2">
+    <Decl id="h0" name="x">
+      <CONST id="i0" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R.con"/>
+    </Decl>
+    <Goal>
+      <APPLY id="i2" sort="Type">
+        <MUTIND id="i4" noType="0" uri="cic:/Coq/Init/Logic_Type/eqT.ind"/>
+        <CONST id="i12" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R.con"/>
+        <REL binder="x" id="i14" idref="h0" sort="Type" value="1"/>
+        <APPLY id="i16" sort="Type">
+          <CONST id="i18" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rdiv.con"/>
+          <APPLY id="i24" sort="Type">
+            <CONST id="i26" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rminus.con"/>
+            <APPLY id="i32" sort="Type">
+              <CONST id="i34" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rminus.con"/>
+              <APPLY id="i40" sort="Type">
+                <CONST id="i42" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rmult.con"/>
+                <APPLY id="i48" sort="Type">
+                  <CONST id="i50" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rplus.con"/>
+                  <REL binder="x" id="i56" idref="h0" sort="Type" value="1"/>
+                  <CONST id="i58" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
+                </APPLY>
+                <APPLY id="i60" sort="Type">
+                  <CONST id="i62" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rplus.con"/>
+                  <REL binder="x" id="i68" idref="h0" sort="Type" value="1"/>
+                  <CONST id="i70" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
+                </APPLY>
+              </APPLY>
+              <CONST id="i72" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
+            </APPLY>
+            <APPLY id="i74" sort="Type">
+              <CONST id="i76" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rmult.con"/>
+              <REL binder="x" id="i82" idref="h0" sort="Type" value="1"/>
+              <REL binder="x" id="i84" idref="h0" sort="Type" value="1"/>
+            </APPLY>
+          </APPLY>
+          <APPLY id="i86" sort="Type">
+            <CONST id="i88" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/Rplus.con"/>
+            <CONST id="i94" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
+            <CONST id="i96" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R1.con"/>
+          </APPLY>
+        </APPLY>
+      </APPLY>
+    </Goal>
+  </Conjecture>
+  <body>
+    <LAMBDA sort="Prop">
+      <decl binder="x" id="i98" type="Type">
+        <CONST id="i162" sort="Type" uri="cic:/Coq/Reals/Rdefinitions/R.con"/>
+      </decl>
+      <target>
+        <META id="i130" no="2" sort="Prop">
+          <substitution>
+            <REL binder="x" id="i160" idref="i98" sort="Type" value="1"/>
+          </substitution>
+        </META>
+      </target>
+    </LAMBDA>
+  </body>
+</CurrentProof>
+</gTopLevelStatus>
+</start_musing>