+++ /dev/null
-<?xml version="1.0" encoding="iso-8859-1"?>
-<?cocoon-format type="text/xhtml"?>
-<m:math xmlns:helm="http://www.cs.unibo.it/helm" xmlns:m="http://www.w3.org/1998/Math/MathML">
- <m:mtable helm:xref="i0" columnalign="left" equalrows="false" align="baseline 1">
- <m:mtr>
- <m:mtd>
- <m:mrow>
- <m:mtext>DEFINITION and_ind() OF TYPE</m:mtext>
- </m:mrow>
- </m:mtd>
- </m:mtr>
- <m:mtr>
- <m:mtd>
- <m:mrow>
- <m:mphantom>
- <m:mtext>__</m:mtext>
- </m:mphantom>
- <m:semantics xmlns:xlink="http://www.w3.org/1999/xlink">
- <m:mrow helm:xref="i22">
- <m:mtable columnalign="left" equalrows="false" align="baseline 1">
- <m:mtr>
- <m:mtd>
- <m:mrow>
- <m:mo stretchy="false">(</m:mo>
- <m:mrow helm:xref="i23">
- <m:mtable columnalign="left" equalrows="false" align="baseline 1">
- <m:mtr>
- <m:mtd>
- <m:mo color="Blue">Π</m:mo>
- <m:mi>A</m:mi>
- <m:mo>:</m:mo>
- <m:mrow helm:xref="i24">
- <m:mo>Prop</m:mo>
- </m:mrow>
- </m:mtd>
- </m:mtr>
- <m:mtr>
- <m:mtd>
- <m:mrow>
- <m:mo>.</m:mo>
- <m:mrow helm:xref="i25">
- <m:mtable columnalign="left" equalrows="false" align="baseline 1">
- <m:mtr>
- <m:mtd>
- <m:mo color="Blue">Π</m:mo>
- <m:mi>B</m:mi>
- <m:mo>:</m:mo>
- <m:mrow helm:xref="i26">
- <m:mo>Prop</m:mo>
- </m:mrow>
- </m:mtd>
- </m:mtr>
- <m:mtr>
- <m:mtd>
- <m:mrow>
- <m:mo>.</m:mo>
- <m:mrow helm:xref="i27">
- <m:mtable columnalign="left" equalrows="false" align="baseline 1">
- <m:mtr>
- <m:mtd>
- <m:mo color="Blue">Π</m:mo>
- <m:mi>P</m:mi>
- <m:mo>:</m:mo>
- <m:mrow helm:xref="i28">
- <m:mo>Prop</m:mo>
- </m:mrow>
- </m:mtd>
- </m:mtr>
- <m:mtr>
- <m:mtd>
- <m:mrow>
- <m:mo>.</m:mo>
- <m:mrow helm:xref="i29">
- <m:mtable columnalign="left" equalrows="false" align="baseline 1">
- <m:mtr>
- <m:mtd>
- <m:mo color="Blue">Π</m:mo>
- <m:mi>f</m:mi>
- <m:mo>:</m:mo>
- <m:mrow helm:xref="i30">
- <m:mo stretchy="false">(</m:mo>
- <m:mi helm:xref="i31">A</m:mi>
- <m:mo color="Blue">→</m:mo>
- <m:mrow helm:xref="i32">
- <m:mo stretchy="false">(</m:mo>
- <m:mi helm:xref="i33">B</m:mi>
- <m:mo color="Blue">→</m:mo>
- <m:mi helm:xref="i34">P</m:mi>
- <m:mo stretchy="false">)</m:mo>
- </m:mrow>
- <m:mo stretchy="false">)</m:mo>
- </m:mrow>
- </m:mtd>
- </m:mtr>
- <m:mtr>
- <m:mtd>
- <m:mrow>
- <m:mo>.</m:mo>
- <m:mrow helm:xref="i35">
- <m:mo color="Blue">Π</m:mo>
- <m:mi>a</m:mi>
- <m:mo>:</m:mo>
- <m:mrow helm:xref="i36">
- <m:mo stretchy="false">(</m:mo>
- <m:mi xlink:href="cic:/coq/INIT/Logic/Conjunction/and.ind" helm:xref="i37">and</m:mi>
- <m:mphantom>
- <m:mtext>_</m:mtext>
- </m:mphantom>
- <m:mi helm:xref="i38">A</m:mi>
- <m:mphantom>
- <m:mtext>_</m:mtext>
- </m:mphantom>
- <m:mi helm:xref="i39">B</m:mi>
- <m:mo stretchy="false">)</m:mo>
- </m:mrow>
- <m:mo>.</m:mo>
- <m:mi helm:xref="i40">P</m:mi>
- </m:mrow>
- </m:mrow>
- </m:mtd>
- </m:mtr>
- </m:mtable>
- </m:mrow>
- </m:mrow>
- </m:mtd>
- </m:mtr>
- </m:mtable>
- </m:mrow>
- </m:mrow>
- </m:mtd>
- </m:mtr>
- </m:mtable>
- </m:mrow>
- </m:mrow>
- </m:mtd>
- </m:mtr>
- </m:mtable>
- </m:mrow>
- </m:mrow>
- </m:mtd>
- </m:mtr>
- <m:mtr>
- <m:mtd>
- <m:mrow>
- <m:mo color="#b03060">:></m:mo>
- <m:mrow helm:xref="i41">
- <m:mo>Prop</m:mo>
- </m:mrow>
- </m:mrow>
- </m:mtd>
- </m:mtr>
- <m:mtr>
- <m:mtd>
- <m:mrow>
- <m:mo stretchy="false">)</m:mo>
- </m:mrow>
- </m:mtd>
- </m:mtr>
- </m:mtable>
- </m:mrow>
- <m:annotation-xml encoding="MathML">
- <m:apply helm:xref="i22">
- <m:csymbol>cast</m:csymbol>
- <m:apply helm:xref="i23">
- <m:csymbol>prod</m:csymbol>
- <m:bvar>
- <m:ci>A</m:ci>
- <m:type>
- <m:apply helm:xref="i24">
- <m:csymbol>Prop</m:csymbol>
- </m:apply>
- </m:type>
- </m:bvar>
- <m:apply helm:xref="i25">
- <m:csymbol>prod</m:csymbol>
- <m:bvar>
- <m:ci>B</m:ci>
- <m:type>
- <m:apply helm:xref="i26">
- <m:csymbol>Prop</m:csymbol>
- </m:apply>
- </m:type>
- </m:bvar>
- <m:apply helm:xref="i27">
- <m:csymbol>prod</m:csymbol>
- <m:bvar>
- <m:ci>P</m:ci>
- <m:type>
- <m:apply helm:xref="i28">
- <m:csymbol>Prop</m:csymbol>
- </m:apply>
- </m:type>
- </m:bvar>
- <m:apply helm:xref="i29">
- <m:csymbol>prod</m:csymbol>
- <m:bvar>
- <m:ci>f</m:ci>
- <m:type>
- <m:apply helm:xref="i30">
- <m:csymbol>arrow</m:csymbol>
- <m:ci helm:xref="i31">A</m:ci>
- <m:apply helm:xref="i32">
- <m:csymbol>arrow</m:csymbol>
- <m:ci helm:xref="i33">B</m:ci>
- <m:ci helm:xref="i34">P</m:ci>
- </m:apply>
- </m:apply>
- </m:type>
- </m:bvar>
- <m:apply helm:xref="i35">
- <m:csymbol>prod</m:csymbol>
- <m:bvar>
- <m:ci>a</m:ci>
- <m:type>
- <m:apply helm:xref="i36">
- <m:csymbol>app</m:csymbol>
- <m:ci definitionURL="cic:/coq/INIT/Logic/Conjunction/and.ind" helm:xref="i37">and</m:ci>
- <m:ci helm:xref="i38">A</m:ci>
- <m:ci helm:xref="i39">B</m:ci>
- </m:apply>
- </m:type>
- </m:bvar>
- <m:ci helm:xref="i40">P</m:ci>
- </m:apply>
- </m:apply>
- </m:apply>
- </m:apply>
- </m:apply>
- <m:apply helm:xref="i41">
- <m:csymbol>Prop</m:csymbol>
- </m:apply>
- </m:apply>
- </m:annotation-xml>
- </m:semantics>
- </m:mrow>
- </m:mtd>
- </m:mtr>
- <m:mtr>
- <m:mtd>
- <m:mrow>
- <m:mtext>AS</m:mtext>
- </m:mrow>
- </m:mtd>
- </m:mtr>
- <m:mtr>
- <m:mtd>
- <m:mrow>
- <m:mphantom>
- <m:mtext>__</m:mtext>
- </m:mphantom>
- <m:semantics xmlns:xlink="http://www.w3.org/1999/xlink">
- <m:mrow helm:xref="i1">
- <m:mtable columnalign="left" equalrows="false" align="baseline 1">
- <m:mtr>
- <m:mtd>
- <m:mo color="Red">λ</m:mo>
- <m:mi>A</m:mi>
- <m:mo>:</m:mo>
- <m:mrow helm:xref="i2">
- <m:mo>Prop</m:mo>
- </m:mrow>
- </m:mtd>
- </m:mtr>
- <m:mtr>
- <m:mtd>
- <m:mrow>
- <m:mo>.</m:mo>
- <m:mrow helm:xref="i3">
- <m:mtable columnalign="left" equalrows="false" align="baseline 1">
- <m:mtr>
- <m:mtd>
- <m:mo color="Red">λ</m:mo>
- <m:mi>B</m:mi>
- <m:mo>:</m:mo>
- <m:mrow helm:xref="i4">
- <m:mo>Prop</m:mo>
- </m:mrow>
- </m:mtd>
- </m:mtr>
- <m:mtr>
- <m:mtd>
- <m:mrow>
- <m:mo>.</m:mo>
- <m:mrow helm:xref="i5">
- <m:mtable columnalign="left" equalrows="false" align="baseline 1">
- <m:mtr>
- <m:mtd>
- <m:mo color="Red">λ</m:mo>
- <m:mi>P</m:mi>
- <m:mo>:</m:mo>
- <m:mrow helm:xref="i6">
- <m:mo>Prop</m:mo>
- </m:mrow>
- </m:mtd>
- </m:mtr>
- <m:mtr>
- <m:mtd>
- <m:mrow>
- <m:mo>.</m:mo>
- <m:mrow helm:xref="i7">
- <m:mtable columnalign="left" equalrows="false" align="baseline 1">
- <m:mtr>
- <m:mtd>
- <m:mo color="Red">λ</m:mo>
- <m:mi>f</m:mi>
- <m:mo>:</m:mo>
- <m:mrow helm:xref="i8">
- <m:mo stretchy="false">(</m:mo>
- <m:mi helm:xref="i9">A</m:mi>
- <m:mo color="Blue">→</m:mo>
- <m:mrow helm:xref="i10">
- <m:mo stretchy="false">(</m:mo>
- <m:mi helm:xref="i11">B</m:mi>
- <m:mo color="Blue">→</m:mo>
- <m:mi helm:xref="i12">P</m:mi>
- <m:mo stretchy="false">)</m:mo>
- </m:mrow>
- <m:mo stretchy="false">)</m:mo>
- </m:mrow>
- </m:mtd>
- </m:mtr>
- <m:mtr>
- <m:mtd>
- <m:mrow>
- <m:mo>.</m:mo>
- <m:mrow helm:xref="i13">
- <m:mtable columnalign="left" equalrows="false" align="baseline 1">
- <m:mtr>
- <m:mtd>
- <m:mo color="Red">λ</m:mo>
- <m:mi>a</m:mi>
- <m:mo>:</m:mo>
- <m:mrow helm:xref="i14">
- <m:mo stretchy="false">(</m:mo>
- <m:mi xlink:href="cic:/coq/INIT/Logic/Conjunction/and.ind" helm:xref="i15">and</m:mi>
- <m:mphantom>
- <m:mtext>_</m:mtext>
- </m:mphantom>
- <m:mi helm:xref="i16">A</m:mi>
- <m:mphantom>
- <m:mtext>_</m:mtext>
- </m:mphantom>
- <m:mi helm:xref="i17">B</m:mi>
- <m:mo stretchy="false">)</m:mo>
- </m:mrow>
- </m:mtd>
- </m:mtr>
- <m:mtr>
- <m:mtd>
- <m:mrow>
- <m:mo>.</m:mo>
- <m:mrow helm:xref="i18">
- <m:mo><</m:mo>
- <m:mi helm:xref="i19">P</m:mi>
- <m:mo>></m:mo>
- <m:mo>CASES</m:mo>
- <m:mphantom>
- <m:mtext>_</m:mtext>
- </m:mphantom>
- <m:mi helm:xref="i20">a</m:mi>
- <m:mphantom>
- <m:mtext>_</m:mtext>
- </m:mphantom>
- <m:mo>OF</m:mo>
- <m:mrow>
- <m:mo stretchy="false">(</m:mo>
- <m:mi>conj</m:mi>
- <m:mphantom>
- <m:mtext>_</m:mtext>
- </m:mphantom>
- <m:mi>$1</m:mi>
- <m:mphantom>
- <m:mtext>_</m:mtext>
- </m:mphantom>
- <m:mi>$2</m:mi>
- <m:mo stretchy="false">)</m:mo>
- </m:mrow>
- <m:mo color="Green">⇒</m:mo>
- <m:mrow>
- <m:mo stretchy="false">(</m:mo>
- <m:mi helm:xref="i21">f</m:mi>
- <m:mphantom>
- <m:mtext>_</m:mtext>
- </m:mphantom>
- <m:mi>$1</m:mi>
- <m:mphantom>
- <m:mtext>_</m:mtext>
- </m:mphantom>
- <m:mi>$2</m:mi>
- <m:mo stretchy="false">)</m:mo>
- </m:mrow>
- <m:mphantom>
- <m:mtext>_</m:mtext>
- </m:mphantom>
- <m:mo>END</m:mo>
- </m:mrow>
- </m:mrow>
- </m:mtd>
- </m:mtr>
- </m:mtable>
- </m:mrow>
- </m:mrow>
- </m:mtd>
- </m:mtr>
- </m:mtable>
- </m:mrow>
- </m:mrow>
- </m:mtd>
- </m:mtr>
- </m:mtable>
- </m:mrow>
- </m:mrow>
- </m:mtd>
- </m:mtr>
- </m:mtable>
- </m:mrow>
- </m:mrow>
- </m:mtd>
- </m:mtr>
- </m:mtable>
- </m:mrow>
- <m:annotation-xml encoding="MathML">
- <m:lambda helm:xref="i1">
- <m:bvar>
- <m:ci>A</m:ci>
- <m:type>
- <m:apply helm:xref="i2">
- <m:csymbol>Prop</m:csymbol>
- </m:apply>
- </m:type>
- </m:bvar>
- <m:lambda helm:xref="i3">
- <m:bvar>
- <m:ci>B</m:ci>
- <m:type>
- <m:apply helm:xref="i4">
- <m:csymbol>Prop</m:csymbol>
- </m:apply>
- </m:type>
- </m:bvar>
- <m:lambda helm:xref="i5">
- <m:bvar>
- <m:ci>P</m:ci>
- <m:type>
- <m:apply helm:xref="i6">
- <m:csymbol>Prop</m:csymbol>
- </m:apply>
- </m:type>
- </m:bvar>
- <m:lambda helm:xref="i7">
- <m:bvar>
- <m:ci>f</m:ci>
- <m:type>
- <m:apply helm:xref="i8">
- <m:csymbol>arrow</m:csymbol>
- <m:ci helm:xref="i9">A</m:ci>
- <m:apply helm:xref="i10">
- <m:csymbol>arrow</m:csymbol>
- <m:ci helm:xref="i11">B</m:ci>
- <m:ci helm:xref="i12">P</m:ci>
- </m:apply>
- </m:apply>
- </m:type>
- </m:bvar>
- <m:lambda helm:xref="i13">
- <m:bvar>
- <m:ci>a</m:ci>
- <m:type>
- <m:apply helm:xref="i14">
- <m:csymbol>app</m:csymbol>
- <m:ci definitionURL="cic:/coq/INIT/Logic/Conjunction/and.ind" helm:xref="i15">and</m:ci>
- <m:ci helm:xref="i16">A</m:ci>
- <m:ci helm:xref="i17">B</m:ci>
- </m:apply>
- </m:type>
- </m:bvar>
- <m:apply helm:xref="i18">
- <m:csymbol>mutcase</m:csymbol>
- <m:ci helm:xref="i19">P</m:ci>
- <m:ci helm:xref="i20">a</m:ci>
- <m:apply>
- <m:csymbol>app</m:csymbol>
- <m:ci>conj</m:ci>
- <m:ci>$1</m:ci>
- <m:ci>$2</m:ci>
- </m:apply>
- <m:apply>
- <m:csymbol>app</m:csymbol>
- <m:ci helm:xref="i21">f</m:ci>
- <m:ci>$1</m:ci>
- <m:ci>$2</m:ci>
- </m:apply>
- </m:apply>
- </m:lambda>
- </m:lambda>
- </m:lambda>
- </m:lambda>
- </m:lambda>
- </m:annotation-xml>
- </m:semantics>
- </m:mrow>
- </m:mtd>
- </m:mtr>
- </m:mtable>
-</m:math>
projects / helm.git / blobdiff