<map version="1.0.1">
<!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net -->
<node CREATED="1606376695618" ID="ID_1352391000" MODIFIED="1606376704278" TEXT="Galois">
<node CREATED="1606376704806" ID="ID_765661988" MODIFIED="1606376724261" POSITION="right" TEXT="polynominnal equation">
<node CREATED="1606376929822" ID="ID_470208262" MODIFIED="1606376964230" TEXT="permutation of solution"/>
<node CREATED="1606376967368" ID="ID_753384811" MODIFIED="1606376989881" TEXT="permutation group"/>
<node CREATED="1606376992888" ID="ID_904343771" MODIFIED="1606377002273" TEXT="reducing order"/>
</node>
<node CREATED="1606376727933" ID="ID_1615933996" MODIFIED="1606376730351" POSITION="right" TEXT="permutation">
<node CREATED="1606377983762" ID="ID_541308822" MODIFIED="1606377988452" TEXT="mathematical notation">
<node CREATED="1606377988737" ID="ID_872236328" MODIFIED="1606377990116" TEXT="abc"/>
</node>
</node>
<node CREATED="1606376850192" ID="ID_1769513270" MODIFIED="1606376853835" POSITION="right" TEXT="group">
<node CREATED="1606376853836" ID="ID_1566417965" MODIFIED="1606376857323" TEXT="symmetric"/>
<node CREATED="1606376863163" ID="ID_1797364624" MODIFIED="1606376870102" TEXT="commutator"/>
<node CREATED="1606376886069" ID="ID_1581604178" MODIFIED="1606376889986" TEXT="solvable">
<node CREATED="1606376891769" ID="ID_269958268" MODIFIED="1606376910710" TEXT="commutator is singleton"/>
<node CREATED="1606377741327" ID="ID_1136118392" MODIFIED="1606377747155" TEXT="commutator enumeration">
<node CREATED="1606377747156" ID="ID_389205569" MODIFIED="1606377753781" TEXT="just a calcuration"/>
<node CREATED="1606377754818" ID="ID_767647256" MODIFIED="1606377760601" TEXT="is that a proof?">
<node CREATED="1606378353555" ID="ID_1858190223" MODIFIED="1606378362619" TEXT="first list contains everything"/>
<node CREATED="1606378363564" ID="ID_188849330" MODIFIED="1606378390432" TEXT="is exact commutator list"/>
<node CREATED="1606378391310" ID="ID_838630093" MODIFIED="1606378455916" TEXT="everything have to be connected"/>
<node CREATED="1606378457553" ID="ID_1529743539" MODIFIED="1606378464964" TEXT="in Agda"/>
</node>
</node>
</node>
</node>
<node CREATED="1606376743358" FOLDED="true" ID="ID_396648943" MODIFIED="1606970261596" POSITION="right" TEXT="Agda">
<node CREATED="1606376745032" ID="ID_1337826128" MODIFIED="1606376830658" TEXT=" constructive logic "/>
<node CREATED="1606376831782" ID="ID_470865242" MODIFIED="1606376838201" TEXT="functional programming language"/>
<node CREATED="1606377112948" ID="ID_898910285" MODIFIED="1606377114878" TEXT="data type">
<node CREATED="1606377114879" ID="ID_1941155842" MODIFIED="1606377118014" TEXT="Data.Fin"/>
<node CREATED="1606377121895" ID="ID_1139692699" MODIFIED="1606377131304" TEXT="Data.Fin.Permutation"/>
<node CREATED="1606377132775" ID="ID_149755525" MODIFIED="1606377139512" TEXT="Data.List.Fresh">
<node CREATED="1606727196377" ID="ID_1375126776" MODIFIED="1606727202570" TEXT="direct write"/>
</node>
<node CREATED="1606377780220" ID="ID_698861196" MODIFIED="1606377792633" TEXT="Data.List Any"/>
</node>
<node CREATED="1606727152968" ID="ID_984157342" MODIFIED="1606727165737" TEXT="data type with ">
<node CREATED="1606727165738" ID="ID_1571937464" MODIFIED="1606727167433" TEXT="proof"/>
<node CREATED="1606727174606" ID="ID_876063224" MODIFIED="1606727178757" TEXT="constraint"/>
</node>
<node CREATED="1606378049124" ID="ID_316648697" MODIFIED="1606378053107" TEXT="Bijection">
<node CREATED="1606378059541" ID="ID_641510883" MODIFIED="1606378065594" TEXT="strange notation"/>
</node>
<node CREATED="1606377647512" ID="ID_109508194" MODIFIED="1606377651001" TEXT="equality">
<node CREATED="1606377651001" ID="ID_1995052319" MODIFIED="1606377653316" TEXT="as Set"/>
<node CREATED="1606377654200" ID="ID_744275621" MODIFIED="1606377660957" TEXT="as Unification"/>
</node>
</node>
<node CREATED="1606377593412" FOLDED="true" ID="ID_998775220" MODIFIED="1606970263675" POSITION="right" TEXT="Galois Theorem">
<node CREATED="1606377617749" ID="ID_833853645" MODIFIED="1606377627175" TEXT="equality on permutation">
<node CREATED="1606377627176" ID="ID_159348794" MODIFIED="1606377629558" TEXT="difficult"/>
</node>
<node CREATED="1606377634711" ID="ID_1966973817" MODIFIED="1606377642062" TEXT="equality on FL">
<node CREATED="1606377642062" ID="ID_918693225" MODIFIED="1606377645984" TEXT="refl"/>
</node>
</node>
<node CREATED="1606377913808" ID="ID_594485495" MODIFIED="1606377920415" POSITION="right" TEXT="analysis">
<node CREATED="1606377921047" ID="ID_827184530" MODIFIED="1606377932723" TEXT="concrete and abstract"/>
<node CREATED="1606377933376" ID="ID_1751276075" MODIFIED="1606377938290" TEXT="dynamic and static"/>
<node CREATED="1606378218212" ID="ID_710334852" MODIFIED="1606378233384" TEXT="unfinished proofs">
<node CREATED="1606378233385" ID="ID_488108201" MODIFIED="1606378236686" TEXT="Any">
<node CREATED="1606378407387" ID="ID_1670776002" MODIFIED="1606378417108" TEXT="carry Any returning function"/>
</node>
<node CREATED="1606378237149" ID="ID_1026280756" MODIFIED="1606378246179" TEXT="Commutator">
<node CREATED="1606727134876" ID="ID_1577934229" MODIFIED="1606727138330" TEXT="done"/>
</node>
<node CREATED="1606378250310" ID="ID_1867193418" MODIFIED="1606378258673" TEXT="computation is possible"/>
</node>
<node CREATED="1606377946668" ID="ID_502942305" MODIFIED="1606377952605" TEXT="computation time">
<node CREATED="1606377952606" ID="ID_530532314" MODIFIED="1606377954403" TEXT="on proof"/>
<node CREATED="1606377955030" ID="ID_1325791815" MODIFIED="1606377958838" TEXT="on enumaration"/>
<node CREATED="1606728034991" ID="ID_864429394" MODIFIED="1606728050441" TEXT="no type inference on computation"/>
<node CREATED="1606728051458" ID="ID_463456042" MODIFIED="1606728057116" TEXT="overhead">
<node CREATED="1606728057117" ID="ID_777871568" MODIFIED="1606728073829" TEXT="what is fresh list?"/>
<node CREATED="1606728079796" ID="ID_480597562" MODIFIED="1606728084210" TEXT="garbage"/>
</node>
</node>
<node CREATED="1606378008534" ID="ID_1589402453" MODIFIED="1606378016376" TEXT="easier solution?">
<node CREATED="1606378016376" ID="ID_1440585232" MODIFIED="1606378026002" TEXT="direct FL injection"/>
<node CREATED="1606378089783" ID="ID_1856387313" MODIFIED="1606378097519" TEXT="define FL-Group">
<node CREATED="1606378102162" ID="ID_644573596" MODIFIED="1606378116983" TEXT="define commutator for it"/>
<node CREATED="1606378133381" ID="ID_732030297" MODIFIED="1606378150072" TEXT="as concrete data "/>
</node>
<node CREATED="1606379185458" ID="ID_116943440" MODIFIED="1606379189022" TEXT="coinduction?"/>
</node>
<node CREATED="1606727239462" ID="ID_56894444" MODIFIED="1606727245853" TEXT="programming tech">
<node CREATED="1606728272433" ID="ID_1678999565" MODIFIED="1606728275384" TEXT="hole">
<node CREATED="1606728276558" ID="ID_1070945075" MODIFIED="1606728283528" TEXT="unfinished proof"/>
</node>
<node CREATED="1606727474640" ID="ID_1396622569" MODIFIED="1606727477580" TEXT="unicode">
<node CREATED="1606727477581" ID="ID_1012474406" MODIFIED="1606727485082" TEXT="like math book"/>
</node>
<node CREATED="1606727246300" ID="ID_1951835354" MODIFIED="1606727254702" TEXT="parallel recursion"/>
<node CREATED="1606727588877" ID="ID_1240709277" MODIFIED="1606727592242" TEXT="equalit">
<node CREATED="1606727592242" ID="ID_1313466010" MODIFIED="1606727596598" TEXT="as refl"/>
<node CREATED="1606727597429" ID="ID_151150017" MODIFIED="1606727600720" TEXT="as data"/>
<node CREATED="1606727601827" ID="ID_474379006" MODIFIED="1606727606619" TEXT="as record"/>
</node>
<node CREATED="1606727260417" ID="ID_805972014" MODIFIED="1606727267607" TEXT="mutual reference">
<node CREATED="1606727295033" ID="ID_232896969" MODIFIED="1606727301472" TEXT="insertFL"/>
<node CREATED="1606727305059" ID="ID_808432820" MODIFIED="1606727314613" TEXT="list and fresh"/>
</node>
<node CREATED="1606727277546" ID="ID_910007043" MODIFIED="1606727280266" TEXT="Any">
<node CREATED="1606727280267" ID="ID_1325857165" MODIFIED="1606727286773" TEXT="insAny"/>
</node>
<node CREATED="1606727343852" ID="ID_1511159834" MODIFIED="1606727347919" TEXT="naming"/>
<node CREATED="1606727349007" ID="ID_296697488" MODIFIED="1606727370890" TEXT="reference in a function">
<node CREATED="1606727370891" ID="ID_402061017" MODIFIED="1606727373382" TEXT="as module"/>
</node>
<node CREATED="1606727379879" ID="ID_1372261696" MODIFIED="1606727386518" TEXT="mononorphism">
<node CREATED="1606727386519" ID="ID_190346980" MODIFIED="1606727391497" TEXT="renaming"/>
<node CREATED="1606727391865" ID="ID_302032810" MODIFIED="1606727394834" TEXT="hiding"/>
</node>
</node>
</node>
<node CREATED="1606377006821" FOLDED="true" ID="ID_1359586090" MODIFIED="1606970253780" POSITION="left" TEXT="implementation">
<node CREATED="1606377015762" ID="ID_287565717" MODIFIED="1606377020854" TEXT="group">
<node CREATED="1606377891530" ID="ID_1217977502" MODIFIED="1606377895546" TEXT="hierarchy"/>
</node>
<node CREATED="1606377021262" ID="ID_618128777" MODIFIED="1606813527167" TEXT="permutation">
<node CREATED="1606377091642" ID="ID_597466250" MODIFIED="1606377110065" TEXT="bijection on Data.Fin">
<node CREATED="1606378591811" ID="ID_1158865640" MODIFIED="1606378598578" TEXT="abstract"/>
</node>
<node CREATED="1606377392195" ID="ID_1921597264" MODIFIED="1606377397374" TEXT="combinator">
<node CREATED="1606377397374" ID="ID_330696821" MODIFIED="1606377403998" TEXT="prep"/>
<node CREATED="1606377426743" ID="ID_1228887457" MODIFIED="1606377430099" TEXT="swap"/>
<node CREATED="1606377451571" ID="ID_478525497" MODIFIED="1606377453688" TEXT="pins"/>
<node CREATED="1606378599458" ID="ID_1582208431" MODIFIED="1606378602838" TEXT="not unique"/>
</node>
<node CREATED="1606377147557" ID="ID_447332615" MODIFIED="1606377174712" TEXT="List &#x2115;">
<node CREATED="1606378608757" ID="ID_608038587" MODIFIED="1606378614329" TEXT="not unique"/>
</node>
<node CREATED="1606377179308" ID="ID_1784079007" MODIFIED="1606377183560" TEXT="FL n">
<node CREATED="1606377183560" ID="ID_1790506416" MODIFIED="1606377199633" TEXT="decremental Data.Fin List">
<node CREATED="1606378617080" ID="ID_665257211" MODIFIED="1606378619230" TEXT="unique"/>
<node CREATED="1606378626590" ID="ID_1530010631" MODIFIED="1606378628302" TEXT="1 to 1"/>
</node>
<node CREATED="1606377458903" ID="ID_767155416" MODIFIED="1606377465105" TEXT="FL n to Perm"/>
<node CREATED="1606377465737" ID="ID_135453080" MODIFIED="1606377469086" TEXT="Perm to FL"/>
<node CREATED="1606377470255" ID="ID_1105006832" MODIFIED="1606377472861" TEXT="iso"/>
<node CREATED="1606377473713" ID="ID_846590614" MODIFIED="1606377475642" TEXT="injection"/>
</node>
<node CREATED="1606377382892" ID="ID_1747777855" MODIFIED="1606377386415" TEXT="conversion">
<node CREATED="1606727219039" ID="ID_932941583" MODIFIED="1606727227206" TEXT="direct refl"/>
</node>
</node>
<node CREATED="1606377221243" ID="ID_1172252989" MODIFIED="1606377228975" TEXT="enumeration of permutation">
<node CREATED="1606377230408" ID="ID_239078628" MODIFIED="1606377235895" TEXT="List"/>
<node CREATED="1606377236436" ID="ID_1866566989" MODIFIED="1606377239550" TEXT="Fresh List">
<node CREATED="1606378273582" ID="ID_536448598" MODIFIED="1606378282243" TEXT="term itself is simple"/>
<node CREATED="1606378284710" ID="ID_334436404" MODIFIED="1606378294962" TEXT="type is complicated"/>
</node>
</node>
<node CREATED="1606377028929" ID="ID_368973198" MODIFIED="1606377032873" TEXT="commutator">
<node CREATED="1606377252812" ID="ID_134730969" MODIFIED="1606377264147" TEXT="generator">
<node CREATED="1606727532690" ID="ID_1941243109" MODIFIED="1606727540677" TEXT="not necessary"/>
</node>
<node CREATED="1606377266582" ID="ID_85252223" MODIFIED="1606377272449" TEXT="cong"/>
</node>
<node CREATED="1606377033697" ID="ID_1847720925" MODIFIED="1606377036804" TEXT="solvable">
<node CREATED="1606377038096" ID="ID_854168913" MODIFIED="1606377049483" TEXT="second order"/>
<node CREATED="1606377050074" ID="ID_795750040" MODIFIED="1606377055050" TEXT="third order">
<node CREATED="1606377679670" ID="ID_1251443358" MODIFIED="1606377695159" TEXT="a lof of easy equation"/>
</node>
<node CREATED="1606377055860" ID="ID_128064534" MODIFIED="1606377059872" TEXT="forth order">
<node CREATED="1606377695633" ID="ID_660493111" MODIFIED="1606377699494" TEXT="too many"/>
<node CREATED="1606377807636" ID="ID_1107095798" MODIFIED="1606377814089" TEXT="use Fresh list"/>
</node>
<node CREATED="1606377067933" ID="ID_1986356" MODIFIED="1606377071318" TEXT="fifth order">
<node CREATED="1606377814808" ID="ID_1761950431" MODIFIED="1606377837816" TEXT="5 contains 3"/>
<node CREATED="1606377838561" ID="ID_649320127" MODIFIED="1606377854524" TEXT="in two different parts"/>
</node>
</node>
<node CREATED="1606377705411" ID="ID_1242936721" MODIFIED="1606377721190" TEXT="solvable by Fresh List">
<node CREATED="1606377721190" ID="ID_228290840" MODIFIED="1606377724012" TEXT="sorted"/>
<node CREATED="1606377861188" ID="ID_55633177" MODIFIED="1606377863199" TEXT="insert"/>
<node CREATED="1606377863601" ID="ID_1234121961" MODIFIED="1606377865965" TEXT="any">
<node CREATED="1606377874500" ID="ID_1547561546" MODIFIED="1606377881123" TEXT="it contains everything?"/>
</node>
</node>
<node CREATED="1606813837317" ID="ID_1335663246" MODIFIED="1606813855860" TEXT="fresh list of all permutation"/>
<node CREATED="1606813857408" ID="ID_648118399" MODIFIED="1606813887836" TEXT="new commutatorfresh  list from fresh list of commutator"/>
<node CREATED="1606377291291" ID="ID_1439868847" MODIFIED="1606813832093" TEXT="Equalizer">
<node CREATED="1606377314717" ID="ID_503791605" MODIFIED="1606377329048" TEXT="equality on concrete object"/>
<node CREATED="1606377330172" ID="ID_1955667161" MODIFIED="1606377336895" TEXT="equality on abstract object"/>
</node>
</node>
<node CREATED="1606378512784" ID="ID_873264480" MODIFIED="1606378523086" POSITION="left" TEXT="paper">
<node CREATED="1606379096805" ID="ID_696482092" MODIFIED="1606379099309" TEXT="problem">
<node CREATED="1606379099309" ID="ID_752930881" MODIFIED="1606379107094" TEXT="enumerating commutator"/>
<node CREATED="1606379107643" ID="ID_1614555070" MODIFIED="1606379117201" TEXT="is this really a proof?"/>
<node CREATED="1606379124041" ID="ID_1678061189" MODIFIED="1606379130309" TEXT="all connected in Agda"/>
</node>
<node CREATED="1606378515709" ID="ID_917416576" MODIFIED="1606378542758" TEXT="Galois introduction">
<node CREATED="1606727909781" ID="ID_1764355857" MODIFIED="1606727916012" TEXT="easy and quick"/>
<node CREATED="1606814040735" ID="ID_719983189" MODIFIED="1606814043031" TEXT="solvable">
<node CREATED="1606814053153" ID="ID_1444282098" MODIFIED="1606814056332" TEXT="commutator">
<node CREATED="1606814056332" ID="ID_1280722589" MODIFIED="1606814079940" TEXT="[ f , g ] = -f -g + f + g"/>
</node>
<node CREATED="1606814095122" ID="ID_56804263" MODIFIED="1606814098749" TEXT="generator">
<node CREATED="1606814099966" ID="ID_274662193" MODIFIED="1606814117737" TEXT="all possible product of commutator "/>
<node CREATED="1606814137761" ID="ID_991170867" MODIFIED="1606814142168" TEXT="not necessary"/>
</node>
</node>
</node>
<node CREATED="1606378543316" ID="ID_434512007" MODIFIED="1606378547552" TEXT="Agda introduction">
<node CREATED="1606378554127" ID="ID_762123734" MODIFIED="1606378563015" TEXT="Group representation"/>
<node CREATED="1606378568196" ID="ID_610013381" MODIFIED="1606378572610" TEXT="Permutation"/>
<node CREATED="1606814013245" ID="ID_1103109909" MODIFIED="1606814017032" TEXT="relation">
<node CREATED="1606814017033" ID="ID_1278020638" MODIFIED="1606814019167" TEXT="data"/>
<node CREATED="1606814019666" ID="ID_931592921" MODIFIED="1606814021966" TEXT="record"/>
</node>
</node>
<node CREATED="1606378575594" ID="ID_1573892815" MODIFIED="1606378585288" TEXT="Representation of Permutation">
<node CREATED="1606378644922" ID="ID_1797326547" MODIFIED="1606378648975" TEXT="math">
<node CREATED="1606378648976" ID="ID_1052913615" MODIFIED="1606378650331" TEXT="abc"/>
</node>
<node CREATED="1606378653895" ID="ID_1900422285" MODIFIED="1606378655245" TEXT="list">
<node CREATED="1606378655246" ID="ID_844966393" MODIFIED="1606378658614" TEXT="not unique"/>
<node CREATED="1606378668243" ID="ID_1727235552" MODIFIED="1606378675693" TEXT="no permutation property"/>
</node>
<node CREATED="1606378662595" ID="ID_1560893595" MODIFIED="1606378666125" TEXT="bijection">
<node CREATED="1606378666126" ID="ID_147732297" MODIFIED="1606378695445" TEXT="abstract"/>
</node>
<node CREATED="1606378701314" ID="ID_1561884094" MODIFIED="1606378706107" TEXT="combinator">
<node CREATED="1606378706108" ID="ID_560079212" MODIFIED="1606378708991" TEXT="not unique"/>
</node>
<node CREATED="1606378715224" ID="ID_1817493034" MODIFIED="1606378717668" TEXT="FL">
<node CREATED="1606378717668" ID="ID_1607834497" MODIFIED="1606378719860" TEXT="unique"/>
<node CREATED="1606378721382" ID="ID_1710096678" MODIFIED="1606378723061" TEXT="1 to 1"/>
</node>
</node>
<node CREATED="1606378927269" ID="ID_1432020010" MODIFIED="1606378933032" TEXT="enumeration of FL">
<node CREATED="1606378933032" ID="ID_124351974" MODIFIED="1606378936038" TEXT="Fresh List"/>
<node CREATED="1606378936579" ID="ID_863395146" MODIFIED="1606378938352" TEXT="Any"/>
</node>
<node CREATED="1606378586134" ID="ID_115815719" MODIFIED="1606378745085" TEXT="Solvable">
<node CREATED="1606378745085" ID="ID_132480944" MODIFIED="1606378748529" TEXT="Commutator"/>
<node CREATED="1606378750600" ID="ID_326008986" MODIFIED="1606378757686" TEXT="Commutator implementationn"/>
</node>
<node CREATED="1606378771575" ID="ID_1064018730" MODIFIED="1606378780946" TEXT="proof os Solvability">
<node CREATED="1606378780946" ID="ID_679164783" MODIFIED="1606378788919" TEXT="on abstract Permutation">
<node CREATED="1606378834624" ID="ID_1953177659" MODIFIED="1606378835927" TEXT="on 2"/>
</node>
<node CREATED="1606378791247" ID="ID_1180179827" MODIFIED="1606378794009" TEXT="using FL">
<node CREATED="1606378809099" ID="ID_1092149501" MODIFIED="1606378817784" TEXT="on 3"/>
<node CREATED="1606378818337" ID="ID_1783576565" MODIFIED="1606378821442" TEXT="on 5"/>
</node>
<node CREATED="1606378801731" ID="ID_699752428" MODIFIED="1606378808475" TEXT="using Fresh List">
<node CREATED="1606378827030" ID="ID_413592226" MODIFIED="1606378829422" TEXT="on 4"/>
</node>
</node>
<node CREATED="1606378844704" ID="ID_1520622758" MODIFIED="1606378848322" TEXT="anaysis">
<node CREATED="1606378848322" ID="ID_471167918" MODIFIED="1606378857868" TEXT="computation time">
<node CREATED="1606728089529" ID="ID_1271917563" MODIFIED="1606728094180" TEXT="overhead"/>
</node>
<node CREATED="1606378865355" ID="ID_913962071" MODIFIED="1606378869923" TEXT="static and dynamic"/>
<node CREATED="1606378872154" ID="ID_1135285650" MODIFIED="1606378879318" TEXT="abstract and concrete"/>
<node CREATED="1606378885692" ID="ID_615335887" MODIFIED="1606378890266" TEXT="data type with proof"/>
<node CREATED="1606727991341" ID="ID_490445683" MODIFIED="1606728003312" TEXT="agda programming tech"/>
</node>
</node>
</node>
</map>