|
0
|
1 <map version="1.0.1">
|
|
|
2 <!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net -->
|
|
|
3 <node CREATED="1606376695618" ID="ID_1352391000" MODIFIED="1606376704278" TEXT="Galois">
|
|
|
4 <node CREATED="1606376704806" ID="ID_765661988" MODIFIED="1606376724261" POSITION="right" TEXT="polynominnal equation">
|
|
|
5 <node CREATED="1606376929822" ID="ID_470208262" MODIFIED="1606376964230" TEXT="permutation of solution"/>
|
|
|
6 <node CREATED="1606376967368" ID="ID_753384811" MODIFIED="1606376989881" TEXT="permutation group"/>
|
|
|
7 <node CREATED="1606376992888" ID="ID_904343771" MODIFIED="1606377002273" TEXT="reducing order"/>
|
|
|
8 </node>
|
|
|
9 <node CREATED="1606376727933" ID="ID_1615933996" MODIFIED="1606376730351" POSITION="right" TEXT="permutation">
|
|
|
10 <node CREATED="1606377983762" ID="ID_541308822" MODIFIED="1606377988452" TEXT="mathematical notation">
|
|
|
11 <node CREATED="1606377988737" ID="ID_872236328" MODIFIED="1606377990116" TEXT="abc"/>
|
|
|
12 </node>
|
|
|
13 </node>
|
|
|
14 <node CREATED="1606376850192" ID="ID_1769513270" MODIFIED="1606376853835" POSITION="right" TEXT="group">
|
|
|
15 <node CREATED="1606376853836" ID="ID_1566417965" MODIFIED="1606376857323" TEXT="symmetric"/>
|
|
|
16 <node CREATED="1606376863163" ID="ID_1797364624" MODIFIED="1606376870102" TEXT="commutator"/>
|
|
|
17 <node CREATED="1606376886069" ID="ID_1581604178" MODIFIED="1606376889986" TEXT="solvable">
|
|
|
18 <node CREATED="1606376891769" ID="ID_269958268" MODIFIED="1606376910710" TEXT="commutator is singleton"/>
|
|
|
19 <node CREATED="1606377741327" ID="ID_1136118392" MODIFIED="1606377747155" TEXT="commutator enumeration">
|
|
|
20 <node CREATED="1606377747156" ID="ID_389205569" MODIFIED="1606377753781" TEXT="just a calcuration"/>
|
|
|
21 <node CREATED="1606377754818" ID="ID_767647256" MODIFIED="1606377760601" TEXT="is that a proof?">
|
|
|
22 <node CREATED="1606378353555" ID="ID_1858190223" MODIFIED="1606378362619" TEXT="first list contains everything"/>
|
|
|
23 <node CREATED="1606378363564" ID="ID_188849330" MODIFIED="1606378390432" TEXT="is exact commutator list"/>
|
|
|
24 <node CREATED="1606378391310" ID="ID_838630093" MODIFIED="1606378455916" TEXT="everything have to be connected"/>
|
|
|
25 <node CREATED="1606378457553" ID="ID_1529743539" MODIFIED="1606378464964" TEXT="in Agda"/>
|
|
|
26 </node>
|
|
|
27 </node>
|
|
|
28 </node>
|
|
|
29 </node>
|
|
3
|
30 <node CREATED="1606376743358" FOLDED="true" ID="ID_396648943" MODIFIED="1606970261596" POSITION="right" TEXT="Agda">
|
|
0
|
31 <node CREATED="1606376745032" ID="ID_1337826128" MODIFIED="1606376830658" TEXT=" constructive logic "/>
|
|
|
32 <node CREATED="1606376831782" ID="ID_470865242" MODIFIED="1606376838201" TEXT="functional programming language"/>
|
|
|
33 <node CREATED="1606377112948" ID="ID_898910285" MODIFIED="1606377114878" TEXT="data type">
|
|
|
34 <node CREATED="1606377114879" ID="ID_1941155842" MODIFIED="1606377118014" TEXT="Data.Fin"/>
|
|
|
35 <node CREATED="1606377121895" ID="ID_1139692699" MODIFIED="1606377131304" TEXT="Data.Fin.Permutation"/>
|
|
|
36 <node CREATED="1606377132775" ID="ID_149755525" MODIFIED="1606377139512" TEXT="Data.List.Fresh">
|
|
|
37 <node CREATED="1606727196377" ID="ID_1375126776" MODIFIED="1606727202570" TEXT="direct write"/>
|
|
|
38 </node>
|
|
|
39 <node CREATED="1606377780220" ID="ID_698861196" MODIFIED="1606377792633" TEXT="Data.List Any"/>
|
|
|
40 </node>
|
|
|
41 <node CREATED="1606727152968" ID="ID_984157342" MODIFIED="1606727165737" TEXT="data type with ">
|
|
|
42 <node CREATED="1606727165738" ID="ID_1571937464" MODIFIED="1606727167433" TEXT="proof"/>
|
|
|
43 <node CREATED="1606727174606" ID="ID_876063224" MODIFIED="1606727178757" TEXT="constraint"/>
|
|
|
44 </node>
|
|
|
45 <node CREATED="1606378049124" ID="ID_316648697" MODIFIED="1606378053107" TEXT="Bijection">
|
|
|
46 <node CREATED="1606378059541" ID="ID_641510883" MODIFIED="1606378065594" TEXT="strange notation"/>
|
|
|
47 </node>
|
|
|
48 <node CREATED="1606377647512" ID="ID_109508194" MODIFIED="1606377651001" TEXT="equality">
|
|
|
49 <node CREATED="1606377651001" ID="ID_1995052319" MODIFIED="1606377653316" TEXT="as Set"/>
|
|
|
50 <node CREATED="1606377654200" ID="ID_744275621" MODIFIED="1606377660957" TEXT="as Unification"/>
|
|
|
51 </node>
|
|
|
52 </node>
|
|
3
|
53 <node CREATED="1606377593412" FOLDED="true" ID="ID_998775220" MODIFIED="1606970263675" POSITION="right" TEXT="Galois Theorem">
|
|
0
|
54 <node CREATED="1606377617749" ID="ID_833853645" MODIFIED="1606377627175" TEXT="equality on permutation">
|
|
|
55 <node CREATED="1606377627176" ID="ID_159348794" MODIFIED="1606377629558" TEXT="difficult"/>
|
|
|
56 </node>
|
|
|
57 <node CREATED="1606377634711" ID="ID_1966973817" MODIFIED="1606377642062" TEXT="equality on FL">
|
|
|
58 <node CREATED="1606377642062" ID="ID_918693225" MODIFIED="1606377645984" TEXT="refl"/>
|
|
|
59 </node>
|
|
|
60 </node>
|
|
|
61 <node CREATED="1606377913808" ID="ID_594485495" MODIFIED="1606377920415" POSITION="right" TEXT="analysis">
|
|
|
62 <node CREATED="1606377921047" ID="ID_827184530" MODIFIED="1606377932723" TEXT="concrete and abstract"/>
|
|
|
63 <node CREATED="1606377933376" ID="ID_1751276075" MODIFIED="1606377938290" TEXT="dynamic and static"/>
|
|
|
64 <node CREATED="1606378218212" ID="ID_710334852" MODIFIED="1606378233384" TEXT="unfinished proofs">
|
|
|
65 <node CREATED="1606378233385" ID="ID_488108201" MODIFIED="1606378236686" TEXT="Any">
|
|
|
66 <node CREATED="1606378407387" ID="ID_1670776002" MODIFIED="1606378417108" TEXT="carry Any returning function"/>
|
|
|
67 </node>
|
|
|
68 <node CREATED="1606378237149" ID="ID_1026280756" MODIFIED="1606378246179" TEXT="Commutator">
|
|
|
69 <node CREATED="1606727134876" ID="ID_1577934229" MODIFIED="1606727138330" TEXT="done"/>
|
|
|
70 </node>
|
|
|
71 <node CREATED="1606378250310" ID="ID_1867193418" MODIFIED="1606378258673" TEXT="computation is possible"/>
|
|
|
72 </node>
|
|
|
73 <node CREATED="1606377946668" ID="ID_502942305" MODIFIED="1606377952605" TEXT="computation time">
|
|
|
74 <node CREATED="1606377952606" ID="ID_530532314" MODIFIED="1606377954403" TEXT="on proof"/>
|
|
|
75 <node CREATED="1606377955030" ID="ID_1325791815" MODIFIED="1606377958838" TEXT="on enumaration"/>
|
|
|
76 <node CREATED="1606728034991" ID="ID_864429394" MODIFIED="1606728050441" TEXT="no type inference on computation"/>
|
|
|
77 <node CREATED="1606728051458" ID="ID_463456042" MODIFIED="1606728057116" TEXT="overhead">
|
|
|
78 <node CREATED="1606728057117" ID="ID_777871568" MODIFIED="1606728073829" TEXT="what is fresh list?"/>
|
|
|
79 <node CREATED="1606728079796" ID="ID_480597562" MODIFIED="1606728084210" TEXT="garbage"/>
|
|
|
80 </node>
|
|
|
81 </node>
|
|
|
82 <node CREATED="1606378008534" ID="ID_1589402453" MODIFIED="1606378016376" TEXT="easier solution?">
|
|
|
83 <node CREATED="1606378016376" ID="ID_1440585232" MODIFIED="1606378026002" TEXT="direct FL injection"/>
|
|
|
84 <node CREATED="1606378089783" ID="ID_1856387313" MODIFIED="1606378097519" TEXT="define FL-Group">
|
|
|
85 <node CREATED="1606378102162" ID="ID_644573596" MODIFIED="1606378116983" TEXT="define commutator for it"/>
|
|
|
86 <node CREATED="1606378133381" ID="ID_732030297" MODIFIED="1606378150072" TEXT="as concrete data "/>
|
|
|
87 </node>
|
|
|
88 <node CREATED="1606379185458" ID="ID_116943440" MODIFIED="1606379189022" TEXT="coinduction?"/>
|
|
|
89 </node>
|
|
|
90 <node CREATED="1606727239462" ID="ID_56894444" MODIFIED="1606727245853" TEXT="programming tech">
|
|
|
91 <node CREATED="1606728272433" ID="ID_1678999565" MODIFIED="1606728275384" TEXT="hole">
|
|
|
92 <node CREATED="1606728276558" ID="ID_1070945075" MODIFIED="1606728283528" TEXT="unfinished proof"/>
|
|
|
93 </node>
|
|
|
94 <node CREATED="1606727474640" ID="ID_1396622569" MODIFIED="1606727477580" TEXT="unicode">
|
|
|
95 <node CREATED="1606727477581" ID="ID_1012474406" MODIFIED="1606727485082" TEXT="like math book"/>
|
|
|
96 </node>
|
|
|
97 <node CREATED="1606727246300" ID="ID_1951835354" MODIFIED="1606727254702" TEXT="parallel recursion"/>
|
|
|
98 <node CREATED="1606727588877" ID="ID_1240709277" MODIFIED="1606727592242" TEXT="equalit">
|
|
|
99 <node CREATED="1606727592242" ID="ID_1313466010" MODIFIED="1606727596598" TEXT="as refl"/>
|
|
|
100 <node CREATED="1606727597429" ID="ID_151150017" MODIFIED="1606727600720" TEXT="as data"/>
|
|
|
101 <node CREATED="1606727601827" ID="ID_474379006" MODIFIED="1606727606619" TEXT="as record"/>
|
|
|
102 </node>
|
|
|
103 <node CREATED="1606727260417" ID="ID_805972014" MODIFIED="1606727267607" TEXT="mutual reference">
|
|
|
104 <node CREATED="1606727295033" ID="ID_232896969" MODIFIED="1606727301472" TEXT="insertFL"/>
|
|
|
105 <node CREATED="1606727305059" ID="ID_808432820" MODIFIED="1606727314613" TEXT="list and fresh"/>
|
|
|
106 </node>
|
|
|
107 <node CREATED="1606727277546" ID="ID_910007043" MODIFIED="1606727280266" TEXT="Any">
|
|
|
108 <node CREATED="1606727280267" ID="ID_1325857165" MODIFIED="1606727286773" TEXT="insAny"/>
|
|
|
109 </node>
|
|
|
110 <node CREATED="1606727343852" ID="ID_1511159834" MODIFIED="1606727347919" TEXT="naming"/>
|
|
|
111 <node CREATED="1606727349007" ID="ID_296697488" MODIFIED="1606727370890" TEXT="reference in a function">
|
|
|
112 <node CREATED="1606727370891" ID="ID_402061017" MODIFIED="1606727373382" TEXT="as module"/>
|
|
|
113 </node>
|
|
|
114 <node CREATED="1606727379879" ID="ID_1372261696" MODIFIED="1606727386518" TEXT="mononorphism">
|
|
|
115 <node CREATED="1606727386519" ID="ID_190346980" MODIFIED="1606727391497" TEXT="renaming"/>
|
|
|
116 <node CREATED="1606727391865" ID="ID_302032810" MODIFIED="1606727394834" TEXT="hiding"/>
|
|
|
117 </node>
|
|
|
118 </node>
|
|
|
119 </node>
|
|
3
|
120 <node CREATED="1606377006821" FOLDED="true" ID="ID_1359586090" MODIFIED="1606970253780" POSITION="left" TEXT="implementation">
|
|
0
|
121 <node CREATED="1606377015762" ID="ID_287565717" MODIFIED="1606377020854" TEXT="group">
|
|
|
122 <node CREATED="1606377891530" ID="ID_1217977502" MODIFIED="1606377895546" TEXT="hierarchy"/>
|
|
|
123 </node>
|
|
|
124 <node CREATED="1606377021262" ID="ID_618128777" MODIFIED="1606813527167" TEXT="permutation">
|
|
|
125 <node CREATED="1606377091642" ID="ID_597466250" MODIFIED="1606377110065" TEXT="bijection on Data.Fin">
|
|
|
126 <node CREATED="1606378591811" ID="ID_1158865640" MODIFIED="1606378598578" TEXT="abstract"/>
|
|
|
127 </node>
|
|
|
128 <node CREATED="1606377392195" ID="ID_1921597264" MODIFIED="1606377397374" TEXT="combinator">
|
|
|
129 <node CREATED="1606377397374" ID="ID_330696821" MODIFIED="1606377403998" TEXT="prep"/>
|
|
|
130 <node CREATED="1606377426743" ID="ID_1228887457" MODIFIED="1606377430099" TEXT="swap"/>
|
|
|
131 <node CREATED="1606377451571" ID="ID_478525497" MODIFIED="1606377453688" TEXT="pins"/>
|
|
|
132 <node CREATED="1606378599458" ID="ID_1582208431" MODIFIED="1606378602838" TEXT="not unique"/>
|
|
|
133 </node>
|
|
|
134 <node CREATED="1606377147557" ID="ID_447332615" MODIFIED="1606377174712" TEXT="List ℕ">
|
|
|
135 <node CREATED="1606378608757" ID="ID_608038587" MODIFIED="1606378614329" TEXT="not unique"/>
|
|
|
136 </node>
|
|
|
137 <node CREATED="1606377179308" ID="ID_1784079007" MODIFIED="1606377183560" TEXT="FL n">
|
|
|
138 <node CREATED="1606377183560" ID="ID_1790506416" MODIFIED="1606377199633" TEXT="decremental Data.Fin List">
|
|
|
139 <node CREATED="1606378617080" ID="ID_665257211" MODIFIED="1606378619230" TEXT="unique"/>
|
|
|
140 <node CREATED="1606378626590" ID="ID_1530010631" MODIFIED="1606378628302" TEXT="1 to 1"/>
|
|
|
141 </node>
|
|
|
142 <node CREATED="1606377458903" ID="ID_767155416" MODIFIED="1606377465105" TEXT="FL n to Perm"/>
|
|
|
143 <node CREATED="1606377465737" ID="ID_135453080" MODIFIED="1606377469086" TEXT="Perm to FL"/>
|
|
|
144 <node CREATED="1606377470255" ID="ID_1105006832" MODIFIED="1606377472861" TEXT="iso"/>
|
|
|
145 <node CREATED="1606377473713" ID="ID_846590614" MODIFIED="1606377475642" TEXT="injection"/>
|
|
|
146 </node>
|
|
|
147 <node CREATED="1606377382892" ID="ID_1747777855" MODIFIED="1606377386415" TEXT="conversion">
|
|
|
148 <node CREATED="1606727219039" ID="ID_932941583" MODIFIED="1606727227206" TEXT="direct refl"/>
|
|
|
149 </node>
|
|
|
150 </node>
|
|
|
151 <node CREATED="1606377221243" ID="ID_1172252989" MODIFIED="1606377228975" TEXT="enumeration of permutation">
|
|
|
152 <node CREATED="1606377230408" ID="ID_239078628" MODIFIED="1606377235895" TEXT="List"/>
|
|
|
153 <node CREATED="1606377236436" ID="ID_1866566989" MODIFIED="1606377239550" TEXT="Fresh List">
|
|
|
154 <node CREATED="1606378273582" ID="ID_536448598" MODIFIED="1606378282243" TEXT="term itself is simple"/>
|
|
|
155 <node CREATED="1606378284710" ID="ID_334436404" MODIFIED="1606378294962" TEXT="type is complicated"/>
|
|
|
156 </node>
|
|
|
157 </node>
|
|
|
158 <node CREATED="1606377028929" ID="ID_368973198" MODIFIED="1606377032873" TEXT="commutator">
|
|
|
159 <node CREATED="1606377252812" ID="ID_134730969" MODIFIED="1606377264147" TEXT="generator">
|
|
|
160 <node CREATED="1606727532690" ID="ID_1941243109" MODIFIED="1606727540677" TEXT="not necessary"/>
|
|
|
161 </node>
|
|
|
162 <node CREATED="1606377266582" ID="ID_85252223" MODIFIED="1606377272449" TEXT="cong"/>
|
|
|
163 </node>
|
|
|
164 <node CREATED="1606377033697" ID="ID_1847720925" MODIFIED="1606377036804" TEXT="solvable">
|
|
|
165 <node CREATED="1606377038096" ID="ID_854168913" MODIFIED="1606377049483" TEXT="second order"/>
|
|
|
166 <node CREATED="1606377050074" ID="ID_795750040" MODIFIED="1606377055050" TEXT="third order">
|
|
|
167 <node CREATED="1606377679670" ID="ID_1251443358" MODIFIED="1606377695159" TEXT="a lof of easy equation"/>
|
|
|
168 </node>
|
|
|
169 <node CREATED="1606377055860" ID="ID_128064534" MODIFIED="1606377059872" TEXT="forth order">
|
|
|
170 <node CREATED="1606377695633" ID="ID_660493111" MODIFIED="1606377699494" TEXT="too many"/>
|
|
|
171 <node CREATED="1606377807636" ID="ID_1107095798" MODIFIED="1606377814089" TEXT="use Fresh list"/>
|
|
|
172 </node>
|
|
|
173 <node CREATED="1606377067933" ID="ID_1986356" MODIFIED="1606377071318" TEXT="fifth order">
|
|
|
174 <node CREATED="1606377814808" ID="ID_1761950431" MODIFIED="1606377837816" TEXT="5 contains 3"/>
|
|
|
175 <node CREATED="1606377838561" ID="ID_649320127" MODIFIED="1606377854524" TEXT="in two different parts"/>
|
|
|
176 </node>
|
|
|
177 </node>
|
|
|
178 <node CREATED="1606377705411" ID="ID_1242936721" MODIFIED="1606377721190" TEXT="solvable by Fresh List">
|
|
|
179 <node CREATED="1606377721190" ID="ID_228290840" MODIFIED="1606377724012" TEXT="sorted"/>
|
|
|
180 <node CREATED="1606377861188" ID="ID_55633177" MODIFIED="1606377863199" TEXT="insert"/>
|
|
|
181 <node CREATED="1606377863601" ID="ID_1234121961" MODIFIED="1606377865965" TEXT="any">
|
|
|
182 <node CREATED="1606377874500" ID="ID_1547561546" MODIFIED="1606377881123" TEXT="it contains everything?"/>
|
|
|
183 </node>
|
|
|
184 </node>
|
|
|
185 <node CREATED="1606813837317" ID="ID_1335663246" MODIFIED="1606813855860" TEXT="fresh list of all permutation"/>
|
|
|
186 <node CREATED="1606813857408" ID="ID_648118399" MODIFIED="1606813887836" TEXT="new commutatorfresh list from fresh list of commutator"/>
|
|
|
187 <node CREATED="1606377291291" ID="ID_1439868847" MODIFIED="1606813832093" TEXT="Equalizer">
|
|
|
188 <node CREATED="1606377314717" ID="ID_503791605" MODIFIED="1606377329048" TEXT="equality on concrete object"/>
|
|
|
189 <node CREATED="1606377330172" ID="ID_1955667161" MODIFIED="1606377336895" TEXT="equality on abstract object"/>
|
|
|
190 </node>
|
|
|
191 </node>
|
|
|
192 <node CREATED="1606378512784" ID="ID_873264480" MODIFIED="1606378523086" POSITION="left" TEXT="paper">
|
|
|
193 <node CREATED="1606379096805" ID="ID_696482092" MODIFIED="1606379099309" TEXT="problem">
|
|
|
194 <node CREATED="1606379099309" ID="ID_752930881" MODIFIED="1606379107094" TEXT="enumerating commutator"/>
|
|
|
195 <node CREATED="1606379107643" ID="ID_1614555070" MODIFIED="1606379117201" TEXT="is this really a proof?"/>
|
|
|
196 <node CREATED="1606379124041" ID="ID_1678061189" MODIFIED="1606379130309" TEXT="all connected in Agda"/>
|
|
|
197 </node>
|
|
|
198 <node CREATED="1606378515709" ID="ID_917416576" MODIFIED="1606378542758" TEXT="Galois introduction">
|
|
|
199 <node CREATED="1606727909781" ID="ID_1764355857" MODIFIED="1606727916012" TEXT="easy and quick"/>
|
|
|
200 <node CREATED="1606814040735" ID="ID_719983189" MODIFIED="1606814043031" TEXT="solvable">
|
|
|
201 <node CREATED="1606814053153" ID="ID_1444282098" MODIFIED="1606814056332" TEXT="commutator">
|
|
|
202 <node CREATED="1606814056332" ID="ID_1280722589" MODIFIED="1606814079940" TEXT="[ f , g ] = -f -g + f + g"/>
|
|
|
203 </node>
|
|
|
204 <node CREATED="1606814095122" ID="ID_56804263" MODIFIED="1606814098749" TEXT="generator">
|
|
|
205 <node CREATED="1606814099966" ID="ID_274662193" MODIFIED="1606814117737" TEXT="all possible product of commutator "/>
|
|
|
206 <node CREATED="1606814137761" ID="ID_991170867" MODIFIED="1606814142168" TEXT="not necessary"/>
|
|
|
207 </node>
|
|
|
208 </node>
|
|
|
209 </node>
|
|
|
210 <node CREATED="1606378543316" ID="ID_434512007" MODIFIED="1606378547552" TEXT="Agda introduction">
|
|
|
211 <node CREATED="1606378554127" ID="ID_762123734" MODIFIED="1606378563015" TEXT="Group representation"/>
|
|
|
212 <node CREATED="1606378568196" ID="ID_610013381" MODIFIED="1606378572610" TEXT="Permutation"/>
|
|
|
213 <node CREATED="1606814013245" ID="ID_1103109909" MODIFIED="1606814017032" TEXT="relation">
|
|
|
214 <node CREATED="1606814017033" ID="ID_1278020638" MODIFIED="1606814019167" TEXT="data"/>
|
|
|
215 <node CREATED="1606814019666" ID="ID_931592921" MODIFIED="1606814021966" TEXT="record"/>
|
|
|
216 </node>
|
|
|
217 </node>
|
|
|
218 <node CREATED="1606378575594" ID="ID_1573892815" MODIFIED="1606378585288" TEXT="Representation of Permutation">
|
|
|
219 <node CREATED="1606378644922" ID="ID_1797326547" MODIFIED="1606378648975" TEXT="math">
|
|
|
220 <node CREATED="1606378648976" ID="ID_1052913615" MODIFIED="1606378650331" TEXT="abc"/>
|
|
|
221 </node>
|
|
|
222 <node CREATED="1606378653895" ID="ID_1900422285" MODIFIED="1606378655245" TEXT="list">
|
|
|
223 <node CREATED="1606378655246" ID="ID_844966393" MODIFIED="1606378658614" TEXT="not unique"/>
|
|
|
224 <node CREATED="1606378668243" ID="ID_1727235552" MODIFIED="1606378675693" TEXT="no permutation property"/>
|
|
|
225 </node>
|
|
|
226 <node CREATED="1606378662595" ID="ID_1560893595" MODIFIED="1606378666125" TEXT="bijection">
|
|
|
227 <node CREATED="1606378666126" ID="ID_147732297" MODIFIED="1606378695445" TEXT="abstract"/>
|
|
|
228 </node>
|
|
|
229 <node CREATED="1606378701314" ID="ID_1561884094" MODIFIED="1606378706107" TEXT="combinator">
|
|
|
230 <node CREATED="1606378706108" ID="ID_560079212" MODIFIED="1606378708991" TEXT="not unique"/>
|
|
|
231 </node>
|
|
|
232 <node CREATED="1606378715224" ID="ID_1817493034" MODIFIED="1606378717668" TEXT="FL">
|
|
|
233 <node CREATED="1606378717668" ID="ID_1607834497" MODIFIED="1606378719860" TEXT="unique"/>
|
|
|
234 <node CREATED="1606378721382" ID="ID_1710096678" MODIFIED="1606378723061" TEXT="1 to 1"/>
|
|
|
235 </node>
|
|
|
236 </node>
|
|
|
237 <node CREATED="1606378927269" ID="ID_1432020010" MODIFIED="1606378933032" TEXT="enumeration of FL">
|
|
|
238 <node CREATED="1606378933032" ID="ID_124351974" MODIFIED="1606378936038" TEXT="Fresh List"/>
|
|
|
239 <node CREATED="1606378936579" ID="ID_863395146" MODIFIED="1606378938352" TEXT="Any"/>
|
|
|
240 </node>
|
|
|
241 <node CREATED="1606378586134" ID="ID_115815719" MODIFIED="1606378745085" TEXT="Solvable">
|
|
|
242 <node CREATED="1606378745085" ID="ID_132480944" MODIFIED="1606378748529" TEXT="Commutator"/>
|
|
|
243 <node CREATED="1606378750600" ID="ID_326008986" MODIFIED="1606378757686" TEXT="Commutator implementationn"/>
|
|
|
244 </node>
|
|
|
245 <node CREATED="1606378771575" ID="ID_1064018730" MODIFIED="1606378780946" TEXT="proof os Solvability">
|
|
|
246 <node CREATED="1606378780946" ID="ID_679164783" MODIFIED="1606378788919" TEXT="on abstract Permutation">
|
|
|
247 <node CREATED="1606378834624" ID="ID_1953177659" MODIFIED="1606378835927" TEXT="on 2"/>
|
|
|
248 </node>
|
|
|
249 <node CREATED="1606378791247" ID="ID_1180179827" MODIFIED="1606378794009" TEXT="using FL">
|
|
|
250 <node CREATED="1606378809099" ID="ID_1092149501" MODIFIED="1606378817784" TEXT="on 3"/>
|
|
|
251 <node CREATED="1606378818337" ID="ID_1783576565" MODIFIED="1606378821442" TEXT="on 5"/>
|
|
|
252 </node>
|
|
|
253 <node CREATED="1606378801731" ID="ID_699752428" MODIFIED="1606378808475" TEXT="using Fresh List">
|
|
|
254 <node CREATED="1606378827030" ID="ID_413592226" MODIFIED="1606378829422" TEXT="on 4"/>
|
|
|
255 </node>
|
|
|
256 </node>
|
|
|
257 <node CREATED="1606378844704" ID="ID_1520622758" MODIFIED="1606378848322" TEXT="anaysis">
|
|
|
258 <node CREATED="1606378848322" ID="ID_471167918" MODIFIED="1606378857868" TEXT="computation time">
|
|
|
259 <node CREATED="1606728089529" ID="ID_1271917563" MODIFIED="1606728094180" TEXT="overhead"/>
|
|
|
260 </node>
|
|
|
261 <node CREATED="1606378865355" ID="ID_913962071" MODIFIED="1606378869923" TEXT="static and dynamic"/>
|
|
|
262 <node CREATED="1606378872154" ID="ID_1135285650" MODIFIED="1606378879318" TEXT="abstract and concrete"/>
|
|
|
263 <node CREATED="1606378885692" ID="ID_615335887" MODIFIED="1606378890266" TEXT="data type with proof"/>
|
|
|
264 <node CREATED="1606727991341" ID="ID_490445683" MODIFIED="1606728003312" TEXT="agda programming tech"/>
|
|
|
265 </node>
|
|
|
266 </node>
|
|
|
267 </node>
|
|
|
268 </map>
|
