# HG changeset patch # User atton # Date 1487402920 -32400 # Node ID 25d0356fc3273da084fec4b5019176aa46720d98 # Parent ba30f79485802edc8b7b6d1a63c9267837532da2 Wrote poster diff -r ba30f7948580 -r 25d0356fc327 poster/atton-poster.graffle/data.plist --- a/poster/atton-poster.graffle/data.plist Sat Feb 18 15:43:30 2017 +0900 +++ b/poster/atton-poster.graffle/data.plist Sat Feb 18 16:28:40 2017 +0900 @@ -14,7 +14,7 @@ BackgroundGraphic Bounds - {{0, 0}, {2027.6220703125, 2860.68505859375}} + {{0, 0}, {4055.244140625, 5721.3701171875}} Class SolidGraphic FontInfo @@ -55,7 +55,7 @@ Bounds - {{1035.1123684830297, 1232.6597550922763}, {964.78997414196579, 228}} + {{1047.81102534807, 2719.1620043914941}, {959.36545032042841, 75}} Class ShapedGraphic FitText @@ -70,7 +70,69 @@ 14 ID - 3463 + 3471 + Style + + fill + + Color + + b + 0.66274500000000003 + g + 1 + r + 1 + + + shadow + + Draws + NO + + stroke + + Draws + NO + + + Text + + Align + 0 + Pad + 0.0 + Text + {\rtf1\ansi\ansicpg1252\cocoartf1504\cocoasubrtf810 +{\fonttbl\f0\fnil\fcharset128 HiraKakuProN-W3;} +{\colortbl;\red255\green255\blue255;} +{\*\expandedcolortbl;;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\partightenfactor0 + +\f0\fs48 \cf0 n-push-pop-type n cn ce st = M.exec (M.csComp (n-pop n) (n-push n)) m \'81\'df m\ +-- goto (pop*n . push*n) mds \'81\'df mds} + VerticalPad + 1 + + + + Bounds + {{1044.1489697708976, 2445.3627891954325}, {978.14778642833062, 228}} + Class + ShapedGraphic + FitText + Vertical + Flow + Resize + FontInfo + + Font + HiraKakuProN-W3 + Size + 14 + + ID + 3470 Style fill @@ -102,11 +164,194 @@ {\*\expandedcolortbl;;} \pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\partightenfactor0 -\f0\fs60 \cf0 \'81\'45Curry-Howard Isomorphism \'82\'c9\'82\'e6\'82\'e8\'8f\'d8\'96\'be\'82\'c6\'83\'76\'83\'8d\'83\'4f\'83\'89\'83\'80\'82\'cc\'8c\'5e\'82\'cd\'91\'ce\'89\'9e\ -\'81\'45\'98\'5f\'97\'9d\'8e\'ae\'82\'cd\'8c\'5e\'82\'c9\'91\'8a\'93\'96\'82\'b5\'81\'41\'8f\'d8\'96\'be\'82\'cd\'82\'bb\'82\'cc\'8c\'5e\'82\'f0\'8e\'9d\'82\'c2\'92\'6c\'82\'cc\'93\'b1\'8f\'6f\ -\'81\'45Coq\'81\'41Agda \'82\'c6\'82\'a2\'82\'c1\'82\'bd\'8b\'ad\'97\'cd\'82\'c8\'8c\'5e\'82\'f0\'8e\'9d\'82\'c2\'8c\'be\'8c\'ea\'82\'c5\'82\'cd\'8f\'d8\'96\'be\'82\'aa\'8b\'4c\'8f\'71\'89\'c2\'94\'5c\ -\'81\'45\'8e\'4f\'92\'69\'98\'5f\'96\'40\'82\'cc\'8e\'a9\'91\'52\'89\'89\'e3\'88\'82\'c9\'82\'e6\'82\'e9\'8f\'d8\'96\'be\'96\'d8\'82\'cd\'88\'c8\'89\'ba\'82\'cc\'82\'e6\'82\'a4\'82\'c9\'82\'c8\'82\'e9\ - - \'8e\'4f\'92\'69\'98\'5f\'96\'40: ((A \'82\'c8\'82\'e7\'82\'ce B) \'82\'a9\'82\'c2 (B \'82\'c8\'82\'e7\'82\'ce C)) \'82\'c8\'82\'e7\'82\'ce (A \'82\'c8\'82\'e7\'82\'ce C)} +\f0\fs60 \cf0 \'81\'45Agda \'82\'c9 CbC \'82\'f0\'95\'cf\'8a\'b7\'82\'b7\'82\'e9\'82\'b1\'82\'c6\'82\'c5\'8f\'d8\'96\'be\'82\'aa\'8d\'73\'82\'c8\'82\'a6\'82\'e9\ +\'81\'45SingleLinkedStack \'82\'c9\'91\'ce\'82\'b7\'82\'e9\'91\'80\'8d\'ec\'82\'cc\'90\'ab\'8e\'bf\'82\'f0\'8f\'d8\'96\'be\'82\'b5\'82\'bd\ +\'81\'45\'81\'75\'82\'a0\'82\'e9\'83\'58\'83\'5e\'83\'62\'83\'4e\'82\'c9\'91\'ce\'82\'b5\'82\'c4n\'89\'f1\'82\'be\'82\'af\'92\'6c\'82\'f0\'90\'cf\'82\'f1\'82\'be\'8c\'e3\'81\'41\ + \'93\'af\'82\'b6\'89\'f1\'90\'94\'82\'be\'82\'af\'92\'6c\'82\'f0\'8e\'e6\'82\'e8\'8f\'6f\'82\'b7\'82\'c6\'8c\'b3\'82\'cc\'83\'58\'83\'5e\'83\'62\'83\'4e\'82\'c9\'93\'99\'82\'b5\'82\'a2\'81\'76\ +\'81\'45Agda \'82\'c5\'90\'ab\'8e\'bf\'82\'f0\'92\'e8\'8b\'60\'82\'b7\'82\'e9\'82\'c6\'88\'c8\'89\'ba\'82\'cc\'82\'e6\'82\'a4\'82\'c9\'82\'c8\'82\'e9} + VerticalPad + 1 + + + + Bounds + {{1053.5401378248487, 2164.7331515077672}, {959.36545032042841, 255}} + Class + ShapedGraphic + FitText + Vertical + Flow + Resize + FontInfo + + Font + HiraKakuProN-W3 + Size + 14 + + ID + 3468 + Style + + fill + + Color + + b + 0.66274500000000003 + g + 1 + r + 1 + + + shadow + + Draws + NO + + stroke + + Draws + NO + + + Text + + Align + 0 + Pad + 0.0 + Text + {\rtf1\ansi\ansicpg1252\cocoartf1504\cocoasubrtf810 +{\fonttbl\f0\fnil\fcharset128 HiraKakuProN-W3;} +{\colortbl;\red255\green255\blue255;} +{\*\expandedcolortbl;;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\partightenfactor0 + +\f0\fs48 \cf0 record ds0 : Set where\ + field\ + a : Int\ + b : Int\ +\ +cs0 : CodeSegment ds0 ds1\ +cs0 = cs (\\d -> goto cs1 (record \{c = (ds0.a d) + (ds0.b d)\}))} + VerticalPad + 1 + + + + Bounds + {{1043.7880980533005, 1772.1407234047856}, {959.36545032042841, 75}} + Class + ShapedGraphic + FitText + Vertical + Flow + Resize + FontInfo + + Font + HiraKakuProN-W3 + Size + 14 + + ID + 3467 + Style + + fill + + Color + + b + 0.66274500000000003 + g + 1 + r + 1 + + + shadow + + Draws + NO + + stroke + + Draws + NO + + + Text + + Align + 0 + Pad + 0.0 + Text + {\rtf1\ansi\ansicpg1252\cocoartf1504\cocoasubrtf810 +{\fonttbl\f0\fnil\fcharset128 HiraKakuProN-W3;} +{\colortbl;\red255\green255\blue255;} +{\*\expandedcolortbl;;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\partightenfactor0 + +\f0\fs48 \cf0 f : \{A B C : Set\} -> ((A -> B) \'81\'7e (B -> C)) -> (A -> C)\ +f = \\p x -> (snd p) ((fst p) x)} + VerticalPad + 1 + + + + Bounds + {{1037.3662304660379, 1705.0393855488203}, {964.78997414196579, 48}} + Class + ShapedGraphic + FitText + Vertical + Flow + Resize + FontInfo + + Font + HiraKakuProN-W3 + Size + 14 + + ID + 3466 + Style + + fill + + Draws + NO + + shadow + + Draws + NO + + stroke + + Draws + NO + + + Text + + Align + 0 + Pad + 0.0 + Text + {\rtf1\ansi\ansicpg1252\cocoartf1504\cocoasubrtf810 +{\fonttbl\f0\fnil\fcharset128 HiraKakuProN-W3;} +{\colortbl;\red255\green255\blue255;} +{\*\expandedcolortbl;;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\partightenfactor0 + +\f0\fs60 \cf0 \'81\'45\'8e\'4f\'92\'69\'98\'5f\'96\'40\'82\'cc Agda \'82\'c9\'82\'e6\'82\'e9\'8f\'d8\'96\'be\'82\'cd\'88\'c8\'89\'ba\'82\'cc\'82\'e6\'82\'a4\'82\'c9\'82\'c8\'82\'e9} VerticalPad 1 @@ -1235,7 +1480,7 @@ Bounds - {{1031.2828257954218, 2403.1111769360605}, {978.14778642833062, 408}} + {{1027.2607383595575, 1971.0188657934857}, {978.14778642833062, 183}} Class ShapedGraphic FitText @@ -1276,16 +1521,16 @@ Pad 0.0 Text - {\rtf1\ansi\ansicpg1252\cocoartf1404\cocoasubrtf340 + {\rtf1\ansi\ansicpg1252\cocoartf1504\cocoasubrtf810 {\fonttbl\f0\fnil\fcharset128 HiraKakuProN-W3;} {\colortbl;\red255\green255\blue255;} +{\*\expandedcolortbl;;} \pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\partightenfactor0 -\f0\fs60 \cf0 \'81\'45\'92\'bc\'90\'da\'83\'41\'83\'5a\'83\'93\'83\'75\'83\'8a\'83\'52\'81\'5b\'83\'68\'82\'f0\'90\'b6\'90\'ac\'82\'b7\'82\'e9builtin\'8a\'d6\'90\'94\'82\'f0\'97\'70\'82\'a2\'82\'e9\'8a\'c2\'8b\'ab\'95\'74\'82\'ab\'8c\'70\'91\'b1\'82\'cc\'8e\'c0\'91\'95\ -\'81\'45data segment \'82\'cc signature \'82\'f0\'97\'98\'97\'70\'82\'b7\'82\'e9\'8d\'5c\'95\'b6\'82\'cc\'90\'dd\'8c\'76\'82\'c6\'8e\'c0\'91\'95\ -\'81\'45meta data segment, meta code segment, data segment \'8c\'fc\'82\'af\'82\'cc\'8d\'5c\'95\'b6\'82\'f0\'83\'52\'83\'93\'83\'70\'83\'43\'83\'89\'8f\'e3\'82\'c9\'8e\'c0\'91\'95\ -\'81\'45C \'82\'c9\'88\'cb\'91\'b6\'82\'b5\'82\'c8\'82\'a2 code segment, data segment \'82\'f0\'97\'70\'82\'a2\'82\'e9\'83\'76\'83\'8d\'83\'4f\'83\'89\'83\'7e\'83\'93\'83\'4f\'8c\'be\'8c\'ea\'82\'cc\'8a\'4a\'94\'ad\ -\'81\'45\'8d\'c5\'93\'4b\'89\'bb\'82\'f0\'82\'a9\'82\'af\'82\'e9\'82\'c6 tail call eliminaition \'82\'aa\'90\'b3\'82\'b5\'82\'ad\'8d\'73\'82\'ed\'82\'ea\'82\'c8\'82\'a2\'83\'6f\'83\'4f\'82\'cc\'8f\'9c\'8b\'8e} +\f0\fs60 \cf0 \'81\'45CbC \'82\'c5 CbC \'8e\'a9\'90\'67\'82\'f0\'8f\'d8\'96\'be\'82\'b5\'82\'bd\'82\'a2\'82\'aa\'8c\'bb\'8f\'f3\'82\'c5\'82\'cd\'82\'c5\'82\'ab\'82\'c8\'82\'a2\ +\'81\'45\'8f\'d8\'96\'be\'8e\'78\'89\'87\'8c\'6e Agda \'8f\'e3\'82\'c5 CbC \'82\'f0\'8b\'4c\'8f\'71\'82\'b7\'82\'e9\'82\'b1\'82\'c6\'82\'c5\'8c\'60\'8e\'ae\'93\'49\'82\'c8\'92\'e8\'8b\'60\'82\'f0\'93\'be\'82\'e9\ +\'81\'45DataSegemnt \'82\'cd\'83\'8c\'83\'52\'81\'5b\'83\'68\'8c\'5e\'82\'c6\'82\'c8\'82\'e8\'81\'41CodeSegment \'82\'cd\'8a\'d6\'90\'94\'8c\'5e\'82\'c6\'82\'c8\'82\'e9\ +\'81\'45\'83\'81\'83\'5e\'8c\'76\'8e\'5a\'82\'cd\'95\'94\'95\'aa\'8c\'5e\'82\'f0\'97\'70\'82\'a2\'82\'e9\'82\'b1\'82\'c6\'82\'c5\'92\'e8\'8b\'60\'89\'c2\'94\'5c} VerticalPad 1 @@ -1297,7 +1542,7 @@ Bounds - {{1108.5131933931748, 2330.1111769360605}, {889.0382080078125, 73}} + {{1111.0752853250578, 1900.0347909289405}, {889.0382080078125, 73}} Class ShapedGraphic FitText @@ -1321,7 +1566,7 @@ 48 ID - 3359 + 3480 Style fill @@ -1353,7 +1598,7 @@ {\*\expandedcolortbl;;} \pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\partightenfactor0 -\f0\fs96 \cf1 \'8d\'a1\'8c\'e3\'82\'cc\'89\'db\'91\'e8} +\f0\fs96 \cf1 Agda \'82\'c6 Continuation based C} VerticalPad 0.0 @@ -1367,11 +1612,11 @@ Class LineGraphic ID - 3361 + 3482 Points - {1048.7219776822747, 2355.6677691298446} - {1091.5672669107641, 2356.4619182321449} + {1051.2840696141577, 1925.5913831227244} + {1094.1293588426472, 1926.3855322250249} Style @@ -1399,7 +1644,7 @@ Tail ID - 3362 + 3483 Position 0.32640770077705383 @@ -1408,13 +1653,13 @@ Class LineGraphic ID - 3362 + 3483 Points - {1042.3300794298798, 2374.9896072795632} - {1054.0592021938141, 2339.5340661031987} - {1056.2400350025155, 2338.2630414925666} - {1078.72100076231, 2338.2630414925666} + {1044.8921713617628, 1944.9132212724428} + {1056.6212941256972, 1909.4576800960788} + {1058.8021269343985, 1908.1866554854466} + {1081.2830926941931, 1908.1866554854466} Style @@ -1442,7 +1687,7 @@ Tail ID - 3363 + 3484 Position 0.25490197539329529 @@ -1451,12 +1696,12 @@ Class LineGraphic ID - 3363 + 3484 Points - {1028.4064583475317, 2374.6607949717227} - {1068.4946853468123, 2375.6074957156529} - {1083.0030894784616, 2374.6607949717227} + {1030.9685502794148, 1944.5844089646025} + {1071.0567772786953, 1945.5311097085328} + {1085.5651814103446, 1944.5844089646025} Style @@ -1484,11 +1729,11 @@ Bounds - {{1024.3427335490621, 2320.1045246080412}, {994.98516845703114, 68}} + {{1026.9048254809452, 1890.0281386009212}, {994.98516845703114, 68}} Class ShapedGraphic ID - 3364 + 3485 Style fill @@ -1530,15 +1775,15 @@ ID - 3360 + 3481 ID - 3358 + 3479 Bounds - {{1022.8641347810715, 2387.7718773267525}, {994.98516845703114, 423.33929960930777}} + {{1028.5875542502738, 1958.518865793493}, {994.98516845703114, 848.51715514332818}} Class ShapedGraphic ID @@ -1558,225 +1803,43 @@ - Bounds - {{1112.5429334301139, 1158.9020555785814}, {889.0382080078125, 73}} - Class - ShapedGraphic - FitText - Vertical - Flow - Resize - FontInfo - - Color - - b - 1 - g - 1 - r - 1 - - Font - HiraKakuProN-W3 - Size - 48 - - ID - 3081 - Style - - fill - - Draws - NO - - shadow - - Draws - NO - - stroke - - Draws - NO - - - Text - - Align - 0 - Pad - 0.0 - Text - {\rtf1\ansi\ansicpg1252\cocoartf1504\cocoasubrtf810 -{\fonttbl\f0\fnil\fcharset128 HiraKakuProN-W3;} -{\colortbl;\red255\green255\blue255;} -{\*\expandedcolortbl;;} -\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\partightenfactor0 - -\f0\fs96 \cf1 Agda \'82\'c6\'92\'e8\'97\'9d\'8f\'d8\'96\'be} - VerticalPad - 0.0 - - - Class Group Graphics - Class - LineGraphic - ID - 3076 - Points - - {1053.9111482845362, 1184.8222610700429} - {1096.7564375130257, 1185.6164101723434} - - Style - - stroke - - Color - - b - 1 - g - 1 - r - 1 - - HeadArrow - FilledBall - Legacy - - TailArrow - 0 - Width - 3 - - - Tail - - ID - 3077 - Position - 0.32640770077705383 - - - - Class - LineGraphic - ID - 3077 - Points - - {1047.5192500321414, 1204.1440992197615} - {1059.2483727960757, 1168.6885580433973} - {1061.4292056047771, 1167.4175334327651} - {1083.9101713645719, 1167.4175334327651} - - Style - - stroke - - Color - - b - 1 - g - 1 - r - 1 - - HeadArrow - FilledBall - Legacy - - TailArrow - 0 - Width - 3 - - - Tail - - ID - 3078 - Position - 0.25490197539329529 - - - - Class - LineGraphic - ID - 3078 - Points - - {1033.5956289497933, 1203.8152869119212} - {1073.6838559490739, 1204.7619876558515} - {1088.1922600807231, 1203.8152869119212} - - Style - - stroke - - Color - - b - 1 - g - 1 - r - 1 - - HeadArrow - FilledBall - Legacy - - TailArrow - 0 - Width - 3 - - - - Bounds - {{1029.5319041513237, 1149.2590165482397}, {994.98516845703114, 68}} + {{1103.0258006042873, 1159.6597550922763}, {889.0382080078125, 73}} Class ShapedGraphic + FitText + Vertical + Flow + Resize + FontInfo + + Color + + b + 1 + g + 1 + r + 1 + + Font + HiraKakuProN-W3 + Size + 48 + ID - 3079 + 3473 Style fill - Color - - b - 0.80000000000000004 - g - 0.59999999999999998 - r - 0.20000000000000001 - - FillType - 2 - GradientAngle - 90 - GradientColor - - b - 0.8 - g - 0.4 - r - 0 - + Draws + NO shadow @@ -1785,14 +1848,205 @@ stroke - Width - 0.5 + Draws + NO + Text + + Align + 0 + Pad + 0.0 + Text + {\rtf1\ansi\ansicpg1252\cocoartf1504\cocoasubrtf810 +{\fonttbl\f0\fnil\fcharset128 HiraKakuProN-W3;} +{\colortbl;\red255\green255\blue255;} +{\*\expandedcolortbl;;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\partightenfactor0 + +\f0\fs96 \cf1 \'92\'e8\'97\'9d\'8f\'d8\'96\'be\'82\'c6\'83\'76\'83\'8d\'83\'4f\'83\'89\'83\'80} + VerticalPad + 0.0 + + + + Class + Group + Graphics + + + Class + LineGraphic + ID + 3475 + Points + + {1044.3940154587096, 1185.5799605837378} + {1087.2393046871991, 1186.3741096860383} + + Style + + stroke + + Color + + b + 1 + g + 1 + r + 1 + + HeadArrow + FilledBall + Legacy + + TailArrow + 0 + Width + 3 + + + Tail + + ID + 3476 + Position + 0.32640770077705383 + + + + Class + LineGraphic + ID + 3476 + Points + + {1038.0021172063148, 1204.9017987334564} + {1049.7312399702491, 1169.4462575570922} + {1051.9120727789505, 1168.17523294646} + {1074.3930385387453, 1168.17523294646} + + Style + + stroke + + Color + + b + 1 + g + 1 + r + 1 + + HeadArrow + FilledBall + Legacy + + TailArrow + 0 + Width + 3 + + + Tail + + ID + 3477 + Position + 0.25490197539329529 + + + + Class + LineGraphic + ID + 3477 + Points + + {1024.0784961239667, 1204.5729864256161} + {1064.1667231232473, 1205.5196871695464} + {1078.6751272548966, 1204.5729864256161} + + Style + + stroke + + Color + + b + 1 + g + 1 + r + 1 + + HeadArrow + FilledBall + Legacy + + TailArrow + 0 + Width + 3 + + + + + Bounds + {{1020.0147713254971, 1150.0167160619346}, {994.98516845703114, 68}} + Class + ShapedGraphic + ID + 3478 + Style + + fill + + Color + + b + 0.80000000000000004 + g + 0.59999999999999998 + r + 0.20000000000000001 + + FillType + 2 + GradientAngle + 90 + GradientColor + + b + 0.8 + g + 0.4 + r + 0 + + + shadow + + Draws + NO + + stroke + + Width + 0.5 + + + + + ID + 3474 ID - 3075 + 3472 Bounds @@ -2862,11 +3116,11 @@ Bounds - {{1027.8490976402113, 1149.2590165482397}, {994.98516845703114, 861.89764395501697}} + {{13.999999719352729, 1578.8976521208529}, {994.98516845703114, 558.42520191707035}} Class ShapedGraphic ID - 3462 + 3262 Style shadow @@ -2883,11 +3137,183 @@ Bounds - {{13.999999719352729, 1578.8976521208529}, {994.98516845703114, 558.42520191707035}} + {{1035.1123684830297, 1232.6597550922763}, {964.78997414196579, 228}} + Class + ShapedGraphic + FitText + Vertical + Flow + Resize + FontInfo + + Font + HiraKakuProN-W3 + Size + 14 + + ID + 3463 + Style + + fill + + Draws + NO + + shadow + + Draws + NO + + stroke + + Draws + NO + + + Text + + Align + 0 + Pad + 0.0 + Text + {\rtf1\ansi\ansicpg1252\cocoartf1504\cocoasubrtf810 +{\fonttbl\f0\fnil\fcharset128 HiraKakuProN-W3;} +{\colortbl;\red255\green255\blue255;} +{\*\expandedcolortbl;;} +\pard\tx560\tx1120\tx1680\tx2240\tx2800\tx3360\tx3920\tx4480\tx5040\tx5600\tx6160\tx6720\pardirnatural\partightenfactor0 + +\f0\fs60 \cf0 \'81\'45Curry-Howard Isomorphism \'82\'c9\'82\'e6\'82\'e8\'8f\'d8\'96\'be\'82\'c6\'83\'76\'83\'8d\'83\'4f\'83\'89\'83\'80\'82\'cc\'8c\'5e\'82\'cd\'91\'ce\'89\'9e\ +\'81\'45\'98\'5f\'97\'9d\'8e\'ae\'82\'cd\'8c\'5e\'82\'c9\'91\'8a\'93\'96\'82\'b5\'81\'41\'8f\'d8\'96\'be\'82\'cd\'82\'bb\'82\'cc\'8c\'5e\'82\'f0\'8e\'9d\'82\'c2\'92\'6c\'82\'cc\'93\'b1\'8f\'6f\ +\'81\'45Coq\'81\'41Agda \'82\'c6\'82\'a2\'82\'c1\'82\'bd\'8b\'ad\'97\'cd\'82\'c8\'8c\'5e\'82\'f0\'8e\'9d\'82\'c2\'8c\'be\'8c\'ea\'82\'c5\'82\'cd\'8f\'d8\'96\'be\'82\'aa\'8b\'4c\'8f\'71\'89\'c2\'94\'5c\ +\'81\'45\'8e\'4f\'92\'69\'98\'5f\'96\'40\'82\'cc\'8e\'a9\'91\'52\'89\'89\'e3\'88\'82\'c9\'82\'e6\'82\'e9\'8f\'d8\'96\'be\'96\'d8\'82\'cd\'88\'c8\'89\'ba\'82\'cc\'82\'e6\'82\'a4\'82\'c9\'82\'c8\'82\'e9\ + - \'8e\'4f\'92\'69\'98\'5f\'96\'40: ((A \'82\'c8\'82\'e7\'82\'ce B) \'82\'a9\'82\'c2 (B \'82\'c8\'82\'e7\'82\'ce C)) \'82\'c8\'82\'e7\'82\'ce (A \'82\'c8\'82\'e7\'82\'ce C)} + VerticalPad + 1 + + + + Bounds + {{742.53629228568104, 1323.9834683055628}, {1568.9763921883164, 2113.4291483889169}} Class ShapedGraphic ID - 3262 + 3464 + ImageID + 28 + ManualSizeImage + YES + Opacity + 0.99999997764825821 + Scale + 2.4999999441206455 + StretchImage + + Style + + fill + + Draws + NO + + shadow + + Draws + NO + + stroke + + Draws + NO + + + + + Bounds + {{1024.0543475942195, 1217.5365689123446}, {994.98516845703114, 650.49494409958015}} + Class + ShapedGraphic + FontInfo + + Font + HiraKakuProN-W3 + Size + 46 + + ID + 3465 + Link + + fileReference + + alias + + AAAAAAH6AAIAAAxNYWNpbnRvc2ggSEQAAAAA + AAAAAAAAAAAAAADUGqDDSCsAAABm8UkRYWth + c2hhUHV0LmdyYWZmbGUAAAAAAAAAAAAAAAAA + AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA + AAAAAAAAAGcXJNTHnRUAAAAAAAAAAP////8A + AAkgAAAAAAAAAAAAAAAAAAAABmltYWdlcwAQ + AAgAANQaIjMAAAARAAgAANTHHoUAAAABACQA + ZvFJAGbUBABRqaYAUamlAB1FUwAbuYwAG7Xa + AAbNyQAGTJ0AAgBsTWFjaW50b3NoIEhEOlVz + ZXJzOgBhdHRvbjoAcmVzZWFyY2g6AGhnOgBQ + YXBlcnM6ADIwMTc6AGF0dG9uLW1hc3RlcjoA + cHJlc2VudGF0aW9uOgBpbWFnZXM6AGFrYXNo + YVB1dC5ncmFmZmxlAA4AJAARAGEAawBhAHMA + aABhAFAAdQB0AC4AZwByAGEAZgBmAGwAZQAP + ABoADABNAGEAYwBpAG4AdABvAHMAaAAgAEgA + RAASAFZVc2Vycy9hdHRvbi9yZXNlYXJjaC9o + Zy9QYXBlcnMvMjAxNy9hdHRvbi1tYXN0ZXIv + cHJlc2VudGF0aW9uL2ltYWdlcy9ha2FzaGFQ + dXQuZ3JhZmZsZQATAAEvAP//AAA= + + bookmark + + Ym9va+wDAAAAAAQQMAAAAAPFOmVt2JcX6S3v + NCx5PiRxV1IG9l4sWCW7xZdgLFp03AIAAAQA + AAADAwAAAAgAKAUAAAABAQAAVXNlcnMAAAAF + AAAAAQEAAGF0dG9uAAAACAAAAAEBAAByZXNl + YXJjaAIAAAABAQAAaGcAAAYAAAABAQAAUGFw + ZXJzAAAEAAAAAQEAADIwMTcMAAAAAQEAAGF0 + dG9uLW1hc3RlcgwAAAABAQAAcHJlc2VudGF0 + aW9uBgAAAAEBAABpbWFnZXMAABEAAAABAQAA + YWthc2hhUHV0LmdyYWZmbGUAAAAoAAAAAQYA + ABAAAAAgAAAAMAAAAEAAAABMAAAAXAAAAGgA + AAB8AAAAkAAAAKAAAAAIAAAABAMAAJ1MBgAA + AAAACAAAAAQDAADJzQYAAAAAAAgAAAAEAwAA + 2rUbAAAAAAAIAAAABAMAAIy5GwAAAAAACAAA + AAQDAABTRR0AAAAAAAgAAAAEAwAApalRAAAA + AAAIAAAABAMAAKapUQAAAAAACAAAAAQDAAAE + 1GYAAAAAAAgAAAAEAwAASfFmAAAAAAAIAAAA + BAMAACQXZwAAAAAAKAAAAAEGAADsAAAA/AAA + AAwBAAAcAQAALAEAADwBAABMAQAAXAEAAGwB + AAB8AQAACAAAAAAEAABBvlGlhQAAABgAAAAB + AgAAAQAAAAAAAAAPAAAAAAAAAAAAAAAAAAAA + CAAAAAQDAAAIAAAAAAAAAAQAAAADAwAA9QEA + AAgAAAABCQAAZmlsZTovLy8MAAAAAQEAAE1h + Y2ludG9zaCBIRAgAAAAEAwAAAACCMXQAAAAI + AAAAAAQAAEG9pKkzAAAAJAAAAAEBAAA0OEIx + NDExNS1DRUU3LTM2MTItOEMwNi1GQ0Q1Qjgy + OTJCQUIYAAAAAQIAAIEAAAABAAAA7xMAAAEA + AAAAAAAAAAAAAAEAAAABAQAALwAAAAAAAAAB + BQAAGgAAAAEBAABOU1VSTERvY3VtZW50SWRl + bnRpZmllcktleQAABAAAAAMDAAA/AAAA2AAA + AP7///8BAAAAAAAAABEAAAAEEAAAvAAAAAAA + AAAFEAAAjAEAAAAAAAAQEAAAzAEAAAAAAABA + EAAAvAEAAAAAAAACIAAAmAIAAAAAAAAFIAAA + CAIAAAAAAAAQIAAAGAIAAAAAAAARIAAATAIA + AAAAAAASIAAALAIAAAAAAAATIAAAPAIAAAAA + AAAgIAAAeAIAAAAAAAAwIAAApAIAAAAAAAAB + wAAA7AEAAAAAAAARwAAAIAAAAAAAAAASwAAA + /AEAAAAAAAAQ0AAABAAAAAAAAACsAgCA0AIA + AAAAAAA= + + path + ../presentation/images/akashaPut.graffle + + Style shadow @@ -2915,18 +3341,20 @@ GuidesVisible YES HPages - 1 + 2 ImageCounter - 28 + 29 ImageLinkBack + ImageList + image28.pdf image27.pdf image24.pdf image23.pdf @@ -2973,7 +3401,7 @@ MasterSheets ModificationDate - 2017-02-18 06:38:01 +0000 + 2017-02-18 07:27:01 +0000 Modifier atton NotesVisible @@ -3046,7 +3474,7 @@ UseEntirePage VPages - 1 + 2 WindowInfo CurrentSheet @@ -3064,15 +3492,15 @@ TopSlabHeight 250 VisibleRegion - {{-281, 334}, {2590, 1886}} + {{146.42857142857144, 1173.2142857142858}, {2312.5, 1683.9285714285716}} Zoom - 0.5 + 0.55999999999999994 ZoomValues Canvas 1 - 0.5 - 0.89999997615814209 + 0.55999999999999994 + 0.78000000000000003 diff -r ba30f7948580 -r 25d0356fc327 poster/atton-poster.graffle/image28.pdf Binary file poster/atton-poster.graffle/image28.pdf has changed diff -r ba30f7948580 -r 25d0356fc327 poster/atton-poster.pdf Binary file poster/atton-poster.pdf has changed diff -r ba30f7948580 -r 25d0356fc327 poster/mcs.pdf Binary file poster/mcs.pdf has changed diff -r ba30f7948580 -r 25d0356fc327 poster/modus-ponens/modus-ponens.svg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/poster/modus-ponens/modus-ponens.svg Sat Feb 18 16:28:40 2017 +0900 @@ -0,0 +1,322 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +