Appendix C Un esempio di file XML per un oggetto CIC
<?xml version="1.0" encoding="ISO-8859-1"?>
<!DOCTYPE Definition SYSTEM "http://localhost:8081/getdtd?url=cic.dtd">
<Definition name="easy" id="i0" params="">
<body>
<LAMBDA id="i1">
<source>
<MUTIND uri="cic:/Datatypes/nat.ind" noType="0" id="i2"/>
</source>
<target binder="n">
<APPLY id="i3">
<CONST uri="cic:/Datatypes/nat_ind.con" id="i4"/>
<LAMBDA id="i5">
<source>
<MUTIND uri="cic:/Datatypes/nat.ind" noType="0" id="i6"/>
</source>
<target binder="n0">
<APPLY id="i7">
<MUTIND uri="cic:/Logic/or.ind" noType="0" id="i8"/>
<APPLY id="i9">
<MUTIND uri="cic:/Logic/eq.ind" noType="0" id="i10"/>
<MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
id="i11"/>
<REL value="1" binder="n0" id="i12"/>
<MUTCONSTRUCT uri="cic:/Datatypes/nat.ind" noType="0"
noConstr="1" id="i13"/>
</APPLY>
<APPLY id="i14">
<MUTIND uri="cic:/Logic/ex.ind" noType="0" id="i15"/>
<MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
id="i16"/>
<LAMBDA id="i17">
<source>
<MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
id="i18"/>
</source>
<target binder="m">
<APPLY id="i19">
<MUTIND uri="cic:/Logic/eq.ind" noType="0"
id="i20"/>
<MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
id="i21"/>
<APPLY id="i22">
<CONST uri="cic:/Peano/plus.con" id="i23"/>
<APPLY id="i24">
<MUTCONSTRUCT uri="cic:/Datatypes/nat.ind"
noType="0" noConstr="2" id="i25"/>
<MUTCONSTRUCT uri="cic:/Datatypes/nat.ind"
noType="0" noConstr="1" id="i26"/>
</APPLY>
<REL value="1" binder="m" id="i27"/>
</APPLY>
<REL value="2" binder="n0" id="i28"/>
</APPLY>
</target>
</LAMBDA>
</APPLY>
</APPLY>
</target>
</LAMBDA>
<APPLY id="i29">
<MUTCONSTRUCT uri="cic:/Logic/or.ind" noType="0"
noConstr="1" id="i30"/>
<APPLY id="i31">
<MUTIND uri="cic:/Logic/eq.ind" noType="0" id="i32"/>
<MUTIND uri="cic:/Datatypes/nat.ind" noType="0" id="i33"/>
<MUTCONSTRUCT uri="cic:/Datatypes/nat.ind" noType="0"
noConstr="1" id="i34"/>
<MUTCONSTRUCT uri="cic:/Datatypes/nat.ind" noType="0"
noConstr="1" id="i35"/>
</APPLY>
<APPLY id="i36">
<MUTIND uri="cic:/Logic/ex.ind" noType="0" id="i37"/>
<MUTIND uri="cic:/Datatypes/nat.ind" noType="0" id="i38"/>
<LAMBDA id="i39">
<source>
<MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
id="i40"/>
</source>
<target binder="m">
<APPLY id="i41">
<MUTIND uri="cic:/Logic/eq.ind" noType="0"
id="i42"/>
<MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
id="i43"/>
<APPLY id="i44">
<CONST uri="cic:/Peano/plus.con" id="i45"/>
<APPLY id="i46">
<MUTCONSTRUCT uri="cic:/Datatypes/nat.ind"
noType="0" noConstr="2" id="i47"/>
<MUTCONSTRUCT uri="cic:/Datatypes/nat.ind"
noType="0" noConstr="1" id="i48"/>
</APPLY>
<REL value="1" binder="m" id="i49"/>
</APPLY>
<MUTCONSTRUCT uri="cic:/Datatypes/nat.ind"
noType="0" noConstr="1" id="i50"/>
</APPLY>
</target>
</LAMBDA>
</APPLY>
<APPLY id="i51">
<MUTCONSTRUCT uri="cic:/Logic/eq.ind" noType="0"
noConstr="1" id="i52"/>
<MUTIND uri="cic:/Datatypes/nat.ind" noType="0" id="i53"/>
<MUTCONSTRUCT uri="cic:/Datatypes/nat.ind" noType="0"
noConstr="1" id="i54"/>
</APPLY>
</APPLY>
<LAMBDA id="i55">
<source>
<MUTIND uri="cic:/Datatypes/nat.ind" noType="0" id="i56"/>
</source>
<target binder="n0">
<LAMBDA id="i57">
<source>
<APPLY id="i58">
<MUTIND uri="cic:/Logic/or.ind" noType="0"
id="i59"/>
<APPLY id="i60">
<MUTIND uri="cic:/Logic/eq.ind" noType="0"
id="i61"/>
<MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
id="i62"/>
<REL value="1" binder="n0" id="i63"/>
<MUTCONSTRUCT uri="cic:/Datatypes/nat.ind"
noType="0" noConstr="1" id="i64"/>
</APPLY>
<APPLY id="i65">
<MUTIND uri="cic:/Logic/ex.ind" noType="0"
id="i66"/>
<MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
id="i67"/>
<LAMBDA id="i68">
<source>
<MUTIND uri="cic:/Datatypes/nat.ind"
noType="0" id="i69"/>
</source>
<target binder="m">
<APPLY id="i70">
<MUTIND uri="cic:/Logic/eq.ind" noType="0"
id="i71"/>
<MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
id="i72"/>
<APPLY id="i73">
<CONST uri="cic:/Peano/plus.con"
id="i74"/>
<APPLY id="i75">
<MUTCONSTRUCT
uri="cic:/Datatypes/nat.ind"
noType="0" noConstr="2" id="i76"/>
<MUTCONSTRUCT
uri="cic:/Datatypes/nat.ind"
noType="0" noConstr="1" id="i77"/>
</APPLY>
<REL value="1" binder="m" id="i78"/>
</APPLY>
<REL value="2" binder="n0" id="i79"/>
</APPLY>
</target>
</LAMBDA>
</APPLY>
</APPLY>
</source>
<target binder="H">
<APPLY id="i80">
<MUTCONSTRUCT uri="cic:/Logic/or.ind" noType="0"
noConstr="2" id="i81"/>
<APPLY id="i82">
<MUTIND uri="cic:/Logic/eq.ind" noType="0"
id="i83"/>
<MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
id="i84"/>
<APPLY id="i85">
<MUTCONSTRUCT uri="cic:/Datatypes/nat.ind"
noType="0" noConstr="2" id="i86"/>
<REL value="2" binder="n0" id="i87"/>
</APPLY>
<MUTCONSTRUCT uri="cic:/Datatypes/nat.ind"
noType="0" noConstr="1" id="i88"/>
</APPLY>
<APPLY id="i89">
<MUTIND uri="cic:/Logic/ex.ind" noType="0"
id="i90"/>
<MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
id="i91"/>
<LAMBDA id="i92">
<source>
<MUTIND uri="cic:/Datatypes/nat.ind"
noType="0" id="i93"/>
</source>
<target binder="m">
<APPLY id="i94">
<MUTIND uri="cic:/Logic/eq.ind" noType="0"
id="i95"/>
<MUTIND uri="cic:/Datatypes/nat.ind"
noType="0" id="i96"/>
<APPLY id="i97">
<CONST
uri="cic:/Peano/plus.con" id="i98"/>
<APPLY id="i99">
<MUTCONSTRUCT
uri="cic:/Datatypes/nat.ind"
noType="0" noConstr="2" id="i100"/>
<MUTCONSTRUCT
uri="cic:/Datatypes/nat.ind"
noType="0" noConstr="1" id="i101"/>
</APPLY>
<REL value="1" binder="m" id="i102"/>
</APPLY>
<APPLY id="i103">
<MUTCONSTRUCT
uri="cic:/Datatypes/nat.ind"
noType="0" noConstr="2" id="i104"/>
<REL value="3" binder="n0" id="i105"/>
</APPLY>
</APPLY>
</target>
</LAMBDA>
</APPLY>
<APPLY id="i106">
<MUTCONSTRUCT uri="cic:/Logic/ex.ind" noType="0"
noConstr="1" id="i107"/>
<MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
id="i108"/>
<LAMBDA id="i109">
<source>
<MUTIND uri="cic:/Datatypes/nat.ind"
noType="0" id="i110"/>
</source>
<target binder="m">
<APPLY id="i111">
<MUTIND uri="cic:/Logic/eq.ind" noType="0"
id="i112"/>
<MUTIND uri="cic:/Datatypes/nat.ind"
noType="0" id="i113"/>
<APPLY id="i114">
<MUTCONSTRUCT
uri="cic:/Datatypes/nat.ind"
noType="0" noConstr="2" id="i115"/>
<REL value="1" binder="m" id="i116"/>
</APPLY>
<APPLY id="i117">
<MUTCONSTRUCT
uri="cic:/Datatypes/nat.ind"
noType="0" noConstr="2" id="i118"/>
<REL value="3" binder="n0" id="i119"/>
</APPLY>
</APPLY>
</target>
</LAMBDA>
<REL value="2" binder="n0" id="i120"/>
<APPLY id="i121">
<MUTCONSTRUCT uri="cic:/Logic/eq.ind"
noType="0" noConstr="1" id="i122"/>
<MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
id="i123"/>
<APPLY id="i124">
<MUTCONSTRUCT uri="cic:/Datatypes/nat.ind"
noType="0" noConstr="2" id="i125"/>
<REL value="2" binder="n0" id="i126"/>
</APPLY>
</APPLY>
</APPLY>
</APPLY>
</target>
</LAMBDA>
</target>
</LAMBDA>
<REL value="1" binder="n" id="i127"/>
</APPLY>
</target>
</LAMBDA>
</body>
<type>
<CAST id="i128">
<term>
<PROD id="i129">
<source>
<MUTIND uri="cic:/Datatypes/nat.ind" noType="0" id="i130"/>
</source>
<target binder="n">
<APPLY id="i131">
<MUTIND uri="cic:/Logic/or.ind" noType="0" id="i132"/>
<APPLY id="i133">
<MUTIND uri="cic:/Logic/eq.ind" noType="0" id="i134"/>
<MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
id="i135"/>
<REL value="1" binder="n" id="i136"/>
<MUTCONSTRUCT uri="cic:/Datatypes/nat.ind" noType="0"
noConstr="1" id="i137"/>
</APPLY>
<APPLY id="i138">
<MUTIND uri="cic:/Logic/ex.ind" noType="0" id="i139"/>
<MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
id="i140"/>
<LAMBDA id="i141">
<source>
<MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
id="i142"/>
</source>
<target binder="m">
<APPLY id="i143">
<MUTIND uri="cic:/Logic/eq.ind" noType="0"
id="i144"/>
<MUTIND uri="cic:/Datatypes/nat.ind" noType="0"
id="i145"/>
<APPLY id="i146">
<CONST uri="cic:/Peano/plus.con" id="i147"/>
<APPLY id="i148">
<MUTCONSTRUCT uri="cic:/Datatypes/nat.ind"
noType="0" noConstr="2" id="i149"/>
<MUTCONSTRUCT uri="cic:/Datatypes/nat.ind"
noType="0" noConstr="1" id="i150"/>
</APPLY>
<REL value="1" binder="m" id="i151"/>
</APPLY>
<REL value="2" binder="n" id="i152"/>
</APPLY>
</target>
</LAMBDA>
</APPLY>
</APPLY>
</target>
</PROD>
</term>
<type>
<SORT value="Prop" id="i153"/>
</type>
</CAST>
</type>
</Definition>