--- a/mindmap/osc2014.mm	Tue May 20 17:51:45 2014 +0900
+++ b/mindmap/osc2014.mm	Wed May 21 19:55:16 2014 +0900
@@ -1,6 +1,6 @@
 <map version="1.0.1">
 <!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net -->
-<node CREATED="1400543905917" ID="ID_572481524" MODIFIED="1400544155826" TEXT="OSC 2014">
+<node CREATED="1400543905917" ID="ID_572481524" MODIFIED="1400668661914" TEXT="OSC 2014">
 <node CREATED="1400543915755" ID="ID_1881286788" MODIFIED="1400543934606" POSITION="right" TEXT="Agda &#x30cd;&#x30bf;">
 <node CREATED="1400543939233" ID="ID_82647617" MODIFIED="1400543946927" TEXT="Peano Arithmetic">
 <node CREATED="1400544002554" ID="ID_1908147492" MODIFIED="1400544012244" TEXT="plus &#x306e;&#x4ea4;&#x63db;&#x6cd5;&#x5247;"/>
@@ -81,5 +81,55 @@
 </node>
 </node>
 </node>
+<node CREATED="1400668663626" ID="ID_515690773" MODIFIED="1400668674190" POSITION="right" TEXT="&#x4f55;&#x3092;&#x308f;&#x304b;&#x3063;&#x3066;&#x3082;&#x3089;&#x3046;&#x304b;">
+<node CREATED="1400669027632" ID="ID_1085165502" MODIFIED="1400669031320" TEXT="bacic of agda">
+<node CREATED="1400669031321" ID="ID_1335142822" MODIFIED="1400669037091" TEXT="type and value"/>
+<node CREATED="1400669040016" ID="ID_1784465189" MODIFIED="1400669045363" TEXT="lambda term"/>
+</node>
+<node CREATED="1400668769696" ID="ID_1216787910" MODIFIED="1400668773939" TEXT="peano arithmetic">
+<node CREATED="1400668874217" ID="ID_657325662" MODIFIED="1400668875283" TEXT="add"/>
+<node CREATED="1400668875848" ID="ID_1416777243" MODIFIED="1400668876555" TEXT="mul"/>
+</node>
+<node CREATED="1400669110897" ID="ID_410845070" MODIFIED="1400669115193" TEXT="operation of agda">
+<node CREATED="1400669054288" ID="ID_101951478" MODIFIED="1400669056059" TEXT="?">
+<node CREATED="1400669058504" ID="ID_577677812" MODIFIED="1400669059691" TEXT="goal"/>
+</node>
+<node CREATED="1400669068408" ID="ID_397237814" MODIFIED="1400669083107" TEXT="normarization">
+<node CREATED="1400669128112" ID="ID_1701331628" MODIFIED="1400669137593" TEXT="1 + 1 = 2"/>
+</node>
+</node>
+<node CREATED="1400669153273" ID="ID_388850162" MODIFIED="1400669164929" TEXT="description of target lemma"/>
+<node CREATED="1400669007079" ID="ID_1284884272" MODIFIED="1400669015667" TEXT="equivalence definition"/>
+<node CREATED="1400668794345" ID="ID_1629665659" MODIFIED="1400668826873" TEXT="equivalence">
+<node CREATED="1400668831080" ID="ID_1585589019" MODIFIED="1400668833099" TEXT="refl"/>
+<node CREATED="1400668833624" ID="ID_1759609548" MODIFIED="1400668838227" TEXT="sym"/>
+<node CREATED="1400668838825" ID="ID_745967048" MODIFIED="1400668840787" TEXT="trans"/>
+</node>
+<node CREATED="1400668706802" ID="ID_1359244831" MODIFIED="1400668744059" TEXT="Reasoning on Agda">
+<node CREATED="1400669556825" ID="ID_1133406151" MODIFIED="1400669561496" TEXT="motivation">
+<node CREATED="1400669561497" ID="ID_1910699629" MODIFIED="1400669573003" TEXT="1 + 2 + 3 = 3 + 3 = 6"/>
+<node CREATED="1400669573952" ID="ID_1325133153" MODIFIED="1400669588298" TEXT="part of equality : 1 + 2 = 3"/>
+</node>
+<node CREATED="1400668748320" ID="ID_1294472557" MODIFIED="1400668752265" TEXT="example">
+<node CREATED="1400669244641" ID="ID_762502821" MODIFIED="1400669252051" TEXT="refl reasoning"/>
+<node CREATED="1400669324920" ID="ID_1483054930" MODIFIED="1400669368609" TEXT="reasoning template"/>
+<node CREATED="1400669305881" ID="ID_970615230" MODIFIED="1400669373873" TEXT="normarization">
+<node CREATED="1400669373873" ID="ID_603853377" MODIFIED="1400669433235" TEXT="start element"/>
+<node CREATED="1400669433616" ID="ID_1227888812" MODIFIED="1400669437355" TEXT="end element"/>
+</node>
+</node>
+<node CREATED="1400668902216" ID="ID_1361569494" MODIFIED="1400668916857" TEXT="lenmma">
+<node CREATED="1400668889305" ID="ID_285305355" MODIFIED="1400668892217" TEXT="add-sym"/>
+<node CREATED="1400668926480" ID="ID_1918706488" MODIFIED="1400668931227" TEXT="add-assoc"/>
+<node CREATED="1400668934776" ID="ID_986075106" MODIFIED="1400668942035" TEXT="add-distribution">
+<node CREATED="1400668949720" ID="ID_1695784338" MODIFIED="1400668953843" TEXT="add-distribution-one"/>
+</node>
+<node CREATED="1400668961584" ID="ID_1753300084" MODIFIED="1400668965986" TEXT="mul-sym">
+<node CREATED="1400669498496" ID="ID_1279020545" MODIFIED="1400669501617" TEXT="target"/>
+</node>
+<node CREATED="1400668982217" ID="ID_346491763" MODIFIED="1400668987081" TEXT="mul-assoc"/>
+</node>
+</node>
+</node>
 </node>
 </map>