<map version="freeplane 1.8.0">
<!--To view this file, download free mind mapping software Freeplane from http://freeplane.sourceforge.net -->
<node TEXT="Galois" FOLDED="false" ID="ID_1352391000" CREATED="1606376695618" MODIFIED="1606376704278"><hook NAME="MapStyle">
    <properties edgeColorConfiguration="#808080ff,#ff0000ff,#0000ffff,#00ff00ff,#ff00ffff,#00ffffff,#7c0000ff,#00007cff,#007c00ff,#7c007cff,#007c7cff,#7c7c00ff" fit_to_viewport="false"/>

<map_styles>
<stylenode LOCALIZED_TEXT="styles.root_node" STYLE="oval" UNIFORM_SHAPE="true" VGAP_QUANTITY="24.0 pt">
<font SIZE="24"/>
<stylenode LOCALIZED_TEXT="styles.predefined" POSITION="right" STYLE="bubble">
<stylenode LOCALIZED_TEXT="default" ICON_SIZE="12.0 pt" COLOR="#000000" STYLE="fork">
<font NAME="SansSerif" SIZE="10" BOLD="false" ITALIC="false"/>
</stylenode>
<stylenode LOCALIZED_TEXT="defaultstyle.details"/>
<stylenode LOCALIZED_TEXT="defaultstyle.attributes">
<font SIZE="9"/>
</stylenode>
<stylenode LOCALIZED_TEXT="defaultstyle.note" COLOR="#000000" BACKGROUND_COLOR="#ffffff" TEXT_ALIGN="LEFT"/>
<stylenode LOCALIZED_TEXT="defaultstyle.floating">
<edge STYLE="hide_edge"/>
<cloud COLOR="#f0f0f0" SHAPE="ROUND_RECT"/>
</stylenode>
</stylenode>
<stylenode LOCALIZED_TEXT="styles.user-defined" POSITION="right" STYLE="bubble">
<stylenode LOCALIZED_TEXT="styles.topic" COLOR="#18898b" STYLE="fork">
<font NAME="Liberation Sans" SIZE="10" BOLD="true"/>
</stylenode>
<stylenode LOCALIZED_TEXT="styles.subtopic" COLOR="#cc3300" STYLE="fork">
<font NAME="Liberation Sans" SIZE="10" BOLD="true"/>
</stylenode>
<stylenode LOCALIZED_TEXT="styles.subsubtopic" COLOR="#669900">
<font NAME="Liberation Sans" SIZE="10" BOLD="true"/>
</stylenode>
<stylenode LOCALIZED_TEXT="styles.important">
<icon BUILTIN="yes"/>
</stylenode>
</stylenode>
<stylenode LOCALIZED_TEXT="styles.AutomaticLayout" POSITION="right" STYLE="bubble">
<stylenode LOCALIZED_TEXT="AutomaticLayout.level.root" COLOR="#000000" STYLE="oval" SHAPE_HORIZONTAL_MARGIN="10.0 pt" SHAPE_VERTICAL_MARGIN="10.0 pt">
<font SIZE="18"/>
</stylenode>
<stylenode LOCALIZED_TEXT="AutomaticLayout.level,1" COLOR="#0033ff">
<font SIZE="16"/>
</stylenode>
<stylenode LOCALIZED_TEXT="AutomaticLayout.level,2" COLOR="#00b439">
<font SIZE="14"/>
</stylenode>
<stylenode LOCALIZED_TEXT="AutomaticLayout.level,3" COLOR="#990000">
<font SIZE="12"/>
</stylenode>
<stylenode LOCALIZED_TEXT="AutomaticLayout.level,4" COLOR="#111111">
<font SIZE="10"/>
</stylenode>
<stylenode LOCALIZED_TEXT="AutomaticLayout.level,5"/>
<stylenode LOCALIZED_TEXT="AutomaticLayout.level,6"/>
<stylenode LOCALIZED_TEXT="AutomaticLayout.level,7"/>
<stylenode LOCALIZED_TEXT="AutomaticLayout.level,8"/>
<stylenode LOCALIZED_TEXT="AutomaticLayout.level,9"/>
<stylenode LOCALIZED_TEXT="AutomaticLayout.level,10"/>
<stylenode LOCALIZED_TEXT="AutomaticLayout.level,11"/>
</stylenode>
</stylenode>
</map_styles>
</hook>
<node TEXT="polynominnal equation" POSITION="right" ID="ID_765661988" CREATED="1606376704806" MODIFIED="1606376724261">
<node TEXT="permutation of solution" ID="ID_470208262" CREATED="1606376929822" MODIFIED="1606376964230"/>
<node TEXT="permutation group" ID="ID_753384811" CREATED="1606376967368" MODIFIED="1606376989881"/>
<node TEXT="reducing order" ID="ID_904343771" CREATED="1606376992888" MODIFIED="1606377002273"/>
</node>
<node TEXT="permutation" POSITION="right" ID="ID_1615933996" CREATED="1606376727933" MODIFIED="1606376730351">
<node TEXT="mathematical notation" ID="ID_541308822" CREATED="1606377983762" MODIFIED="1606377988452">
<node TEXT="abc" ID="ID_872236328" CREATED="1606377988737" MODIFIED="1606377990116"/>
</node>
</node>
<node TEXT="group" FOLDED="true" POSITION="right" ID="ID_1769513270" CREATED="1606376850192" MODIFIED="1606376853835">
<node TEXT="symmetric" ID="ID_1566417965" CREATED="1606376853836" MODIFIED="1606376857323"/>
<node TEXT="commutator" ID="ID_1797364624" CREATED="1606376863163" MODIFIED="1606376870102"/>
<node TEXT="solvable" FOLDED="true" ID="ID_1581604178" CREATED="1606376886069" MODIFIED="1606376889986">
<node TEXT="commutator is singleton" ID="ID_269958268" CREATED="1606376891769" MODIFIED="1606376910710"/>
<node TEXT="commutator enumeration" FOLDED="true" ID="ID_1136118392" CREATED="1606377741327" MODIFIED="1606377747155">
<node TEXT="just a calcuration" ID="ID_389205569" CREATED="1606377747156" MODIFIED="1606377753781"/>
<node TEXT="is that a proof?" FOLDED="true" ID="ID_767647256" CREATED="1606377754818" MODIFIED="1606377760601">
<node TEXT="first list contains everything" ID="ID_1858190223" CREATED="1606378353555" MODIFIED="1606378362619"/>
<node TEXT="is exact commutator list" ID="ID_188849330" CREATED="1606378363564" MODIFIED="1606378390432"/>
<node TEXT="everything have to be connected" ID="ID_838630093" CREATED="1606378391310" MODIFIED="1606378455916"/>
<node TEXT="in Agda" ID="ID_1529743539" CREATED="1606378457553" MODIFIED="1606378464964"/>
</node>
</node>
</node>
</node>
<node TEXT="Agda" FOLDED="true" POSITION="right" ID="ID_396648943" CREATED="1606376743358" MODIFIED="1606376745031">
<node TEXT=" constructive logic " ID="ID_1337826128" CREATED="1606376745032" MODIFIED="1606376830658"/>
<node TEXT="functional programming language" ID="ID_470865242" CREATED="1606376831782" MODIFIED="1606376838201"/>
<node TEXT="data type" FOLDED="true" ID="ID_898910285" CREATED="1606377112948" MODIFIED="1606377114878">
<node TEXT="Data.Fin" ID="ID_1941155842" CREATED="1606377114879" MODIFIED="1606377118014"/>
<node TEXT="Data.Fin.Permutation" ID="ID_1139692699" CREATED="1606377121895" MODIFIED="1606377131304"/>
<node TEXT="Data.List.Fresh" FOLDED="true" ID="ID_149755525" CREATED="1606377132775" MODIFIED="1606377139512">
<node TEXT="direct write" ID="ID_1375126776" CREATED="1606727196377" MODIFIED="1606727202570"/>
</node>
<node TEXT="Data.List Any" ID="ID_698861196" CREATED="1606377780220" MODIFIED="1606377792633"/>
</node>
<node TEXT="data type with " FOLDED="true" ID="ID_984157342" CREATED="1606727152968" MODIFIED="1606727165737">
<node TEXT="proof" ID="ID_1571937464" CREATED="1606727165738" MODIFIED="1606727167433"/>
<node TEXT="constraint" ID="ID_876063224" CREATED="1606727174606" MODIFIED="1606727178757"/>
</node>
<node TEXT="Bijection" FOLDED="true" ID="ID_316648697" CREATED="1606378049124" MODIFIED="1606378053107">
<node TEXT="strange notation" ID="ID_641510883" CREATED="1606378059541" MODIFIED="1606378065594"/>
</node>
<node TEXT="equality" FOLDED="true" ID="ID_109508194" CREATED="1606377647512" MODIFIED="1606377651001">
<node TEXT="as Set" ID="ID_1995052319" CREATED="1606377651001" MODIFIED="1606377653316"/>
<node TEXT="as Unification" ID="ID_744275621" CREATED="1606377654200" MODIFIED="1606377660957"/>
</node>
</node>
<node TEXT="Galois Theorem" FOLDED="true" POSITION="right" ID="ID_998775220" CREATED="1606377593412" MODIFIED="1606377617749">
<node TEXT="equality on permutation" FOLDED="true" ID="ID_833853645" CREATED="1606377617749" MODIFIED="1606377627175">
<node TEXT="difficult" ID="ID_159348794" CREATED="1606377627176" MODIFIED="1606377629558"/>
</node>
<node TEXT="equality on FL" FOLDED="true" ID="ID_1966973817" CREATED="1606377634711" MODIFIED="1606377642062">
<node TEXT="refl" ID="ID_918693225" CREATED="1606377642062" MODIFIED="1606377645984"/>
</node>
</node>
<node TEXT="analysis" FOLDED="true" POSITION="right" ID="ID_594485495" CREATED="1606377913808" MODIFIED="1606377920415">
<node TEXT="concrete and abstract" ID="ID_827184530" CREATED="1606377921047" MODIFIED="1606377932723"/>
<node TEXT="dynamic and static" ID="ID_1751276075" CREATED="1606377933376" MODIFIED="1606377938290"/>
<node TEXT="unfinished proofs" FOLDED="true" ID="ID_710334852" CREATED="1606378218212" MODIFIED="1606378233384">
<node TEXT="Any" FOLDED="true" ID="ID_488108201" CREATED="1606378233385" MODIFIED="1606378236686">
<node TEXT="carry Any returning function" ID="ID_1670776002" CREATED="1606378407387" MODIFIED="1606378417108"/>
</node>
<node TEXT="Commutator" FOLDED="true" ID="ID_1026280756" CREATED="1606378237149" MODIFIED="1606378246179">
<node TEXT="done" ID="ID_1577934229" CREATED="1606727134876" MODIFIED="1606727138330"/>
</node>
<node TEXT="computation is possible" ID="ID_1867193418" CREATED="1606378250310" MODIFIED="1606378258673"/>
</node>
<node TEXT="computation time" FOLDED="true" ID="ID_502942305" CREATED="1606377946668" MODIFIED="1606377952605">
<node TEXT="on proof" ID="ID_530532314" CREATED="1606377952606" MODIFIED="1606377954403"/>
<node TEXT="on enumaration" ID="ID_1325791815" CREATED="1606377955030" MODIFIED="1606377958838"/>
<node TEXT="no type inference on computation" ID="ID_864429394" CREATED="1606728034991" MODIFIED="1606728050441"/>
<node TEXT="overhead" FOLDED="true" ID="ID_463456042" CREATED="1606728051458" MODIFIED="1606728057116">
<node TEXT="what is fresh list?" ID="ID_777871568" CREATED="1606728057117" MODIFIED="1606728073829"/>
<node TEXT="garbage" ID="ID_480597562" CREATED="1606728079796" MODIFIED="1606728084210"/>
</node>
</node>
<node TEXT="easier solution?" FOLDED="true" ID="ID_1589402453" CREATED="1606378008534" MODIFIED="1606378016376">
<node TEXT="direct FL injection" ID="ID_1440585232" CREATED="1606378016376" MODIFIED="1606378026002"/>
<node TEXT="define FL-Group" FOLDED="true" ID="ID_1856387313" CREATED="1606378089783" MODIFIED="1606378097519">
<node TEXT="define commutator for it" ID="ID_644573596" CREATED="1606378102162" MODIFIED="1606378116983"/>
<node TEXT="as concrete data " ID="ID_732030297" CREATED="1606378133381" MODIFIED="1606378150072"/>
</node>
<node TEXT="coinduction?" ID="ID_116943440" CREATED="1606379185458" MODIFIED="1606379189022"/>
</node>
<node TEXT="programming tech" FOLDED="true" ID="ID_56894444" CREATED="1606727239462" MODIFIED="1606727245853">
<node TEXT="hole" FOLDED="true" ID="ID_1678999565" CREATED="1606728272433" MODIFIED="1606728275384">
<node TEXT="unfinished proof" ID="ID_1070945075" CREATED="1606728276558" MODIFIED="1606728283528"/>
</node>
<node TEXT="unicode" FOLDED="true" ID="ID_1396622569" CREATED="1606727474640" MODIFIED="1606727477580">
<node TEXT="like math book" ID="ID_1012474406" CREATED="1606727477581" MODIFIED="1606727485082"/>
</node>
<node TEXT="parallel recursion" ID="ID_1951835354" CREATED="1606727246300" MODIFIED="1606727254702"/>
<node TEXT="equalit" FOLDED="true" ID="ID_1240709277" CREATED="1606727588877" MODIFIED="1606727592242">
<node TEXT="as refl" ID="ID_1313466010" CREATED="1606727592242" MODIFIED="1606727596598"/>
<node TEXT="as data" ID="ID_151150017" CREATED="1606727597429" MODIFIED="1606727600720"/>
<node TEXT="as record" ID="ID_474379006" CREATED="1606727601827" MODIFIED="1606727606619"/>
</node>
<node TEXT="mutual reference" FOLDED="true" ID="ID_805972014" CREATED="1606727260417" MODIFIED="1606727267607">
<node TEXT="insertFL" ID="ID_232896969" CREATED="1606727295033" MODIFIED="1606727301472"/>
<node TEXT="list and fresh" ID="ID_808432820" CREATED="1606727305059" MODIFIED="1606727314613"/>
</node>
<node TEXT="Any" FOLDED="true" ID="ID_910007043" CREATED="1606727277546" MODIFIED="1606727280266">
<node TEXT="insAny" ID="ID_1325857165" CREATED="1606727280267" MODIFIED="1606727286773"/>
</node>
<node TEXT="naming" ID="ID_1511159834" CREATED="1606727343852" MODIFIED="1606727347919"/>
<node TEXT="reference in a function" FOLDED="true" ID="ID_296697488" CREATED="1606727349007" MODIFIED="1606727370890">
<node TEXT="as module" ID="ID_402061017" CREATED="1606727370891" MODIFIED="1606727373382"/>
</node>
<node TEXT="mononorphism" FOLDED="true" ID="ID_1372261696" CREATED="1606727379879" MODIFIED="1606727386518">
<node TEXT="renaming" ID="ID_190346980" CREATED="1606727386519" MODIFIED="1606727391497"/>
<node TEXT="hiding" ID="ID_302032810" CREATED="1606727391865" MODIFIED="1606727394834"/>
</node>
</node>
</node>
<node TEXT="presentation" POSITION="right" ID="ID_1629686657" CREATED="1609990079623" MODIFIED="1609990087321">
<node TEXT="motivation" ID="ID_68741792" CREATED="1609990469910" MODIFIED="1609990474518">
<node TEXT="agda say" ID="ID_1410322270" CREATED="1609990475271" MODIFIED="1609990535394">
<node TEXT="prove all of it" ID="ID_255800370" CREATED="1609990535912" MODIFIED="1609990544007"/>
</node>
<node TEXT="proof carrying data structure" ID="ID_701544233" CREATED="1609990566444" MODIFIED="1609990575065"/>
<node TEXT="all connected" ID="ID_1374956235" CREATED="1609990614612" MODIFIED="1609990619047">
<node TEXT="not only the result" ID="ID_182559689" CREATED="1609990619481" MODIFIED="1609990628683"/>
<node TEXT="the result is proved to be correct" ID="ID_1428974315" CREATED="1609990629258" MODIFIED="1609990638772"/>
<node TEXT="What are you computing?" ID="ID_1070455381" CREATED="1609990639215" MODIFIED="1609990646503"/>
</node>
</node>
<node TEXT="galois theory" ID="ID_808810318" CREATED="1609990087828" MODIFIED="1609990103294">
<node TEXT="polynominal equation" ID="ID_136330816" CREATED="1609990103797" MODIFIED="1609990113989"/>
<node TEXT="symmetric group on solutions" ID="ID_559235306" CREATED="1609990117978" MODIFIED="1609990145025"/>
<node TEXT="group mapping" ID="ID_1179675147" CREATED="1609990150139" MODIFIED="1609990186166"/>
<node TEXT="commutator" ID="ID_226118641" CREATED="1609990196079" MODIFIED="1609990198775"/>
<node TEXT="commutator group" ID="ID_742353850" CREATED="1609990200853" MODIFIED="1609990215758"/>
<node TEXT="solvable" ID="ID_1341500727" CREATED="1609990258050" MODIFIED="1609990261861"/>
</node>
<node TEXT="proof in math text book" ID="ID_789226485" CREATED="1609990263397" MODIFIED="1609990271252"/>
<node TEXT="formalization in agda" ID="ID_202327619" CREATED="1609990273986" MODIFIED="1609990286861">
<node TEXT="agda introduction" ID="ID_35495184" CREATED="1609990288383" MODIFIED="1609990293516">
<node TEXT="lambda" ID="ID_1794615583" CREATED="1609990303910" MODIFIED="1609990309568"/>
<node TEXT="data" ID="ID_1613871642" CREATED="1609990294061" MODIFIED="1609990295779"/>
<node TEXT="record" ID="ID_1150956997" CREATED="1609990296397" MODIFIED="1609990301522"/>
<node TEXT="unification" ID="ID_855340831" CREATED="1609990314851" MODIFIED="1609990323913">
<node TEXT="equation" ID="ID_1714263025" CREATED="1609990324367" MODIFIED="1609990326267"/>
</node>
</node>
<node TEXT="commutator" ID="ID_1080677255" CREATED="1609990330404" MODIFIED="1609990340997">
<node TEXT="Set valued function" ID="ID_477756039" CREATED="1609990341400" MODIFIED="1609990348973"/>
</node>
<node TEXT="solvable" ID="ID_178918488" CREATED="1609990354030" MODIFIED="1609990359075"/>
</node>
<node TEXT="symmetric groupin agda" ID="ID_1083504702" CREATED="1609990379507" MODIFIED="1610005855100">
<node TEXT="representation" ID="ID_319391779" CREATED="1610005856583" MODIFIED="1610005864458">
<node TEXT="Data.Fin" ID="ID_1340949296" CREATED="1609990393883" MODIFIED="1609990404918"/>
<node TEXT="Bijection" ID="ID_316860227" CREATED="1609990405535" MODIFIED="1609990409631"/>
<node TEXT="List" ID="ID_1710126935" CREATED="1609990410154" MODIFIED="1609990413645"/>
<node TEXT="FL" ID="ID_235104633" CREATED="1609990415278" MODIFIED="1609990419436"/>
</node>
<node TEXT="1 to 1" ID="ID_1677442759" CREATED="1610005903688" MODIFIED="1610005907592"/>
</node>
<node TEXT="proofs" ID="ID_1219242238" CREATED="1609992596012" MODIFIED="1609992600251">
<node TEXT="2" OBJECT="java.lang.Long|2" ID="ID_514245484" CREATED="1609992600706" MODIFIED="1609992602407"/>
<node TEXT="injection" ID="ID_1366306030" CREATED="1609992603682" MODIFIED="1609992607205">
<node TEXT="List &lt;-&gt; Permutation" ID="ID_1791881124" CREATED="1609992680676" MODIFIED="1609992688813"/>
<node TEXT="FL &lt;-&gt; Permutation" ID="ID_1601662820" CREATED="1609992667945" MODIFIED="1609992677520"/>
</node>
<node TEXT="3" OBJECT="java.lang.Long|3" ID="ID_1113221609" CREATED="1609992624578" MODIFIED="1609992625803"/>
<node TEXT="5" OBJECT="java.lang.Long|5" ID="ID_1339672501" CREATED="1609992627836" MODIFIED="1609992629038">
<node TEXT="two sym 3" ID="ID_1648879383" CREATED="1609990866219" MODIFIED="1609991318427"/>
</node>
</node>
<node TEXT="a list contains everything" ID="ID_67235294" CREATED="1609990709190" MODIFIED="1609990733750">
<node TEXT="sorted" ID="ID_73107613" CREATED="1609990734279" MODIFIED="1609990738112"/>
<node TEXT="any" ID="ID_1569296473" CREATED="1609990738656" MODIFIED="1609990745411"/>
<node TEXT="enumeration" ID="ID_992373663" CREATED="1610005876529" MODIFIED="1610005884864">
<node TEXT="permutation" ID="ID_535994" CREATED="1610005972212" MODIFIED="1610005978496"/>
<node TEXT="commutator" ID="ID_1725495702" CREATED="1610005979019" MODIFIED="1610005984240"/>
</node>
</node>
<node TEXT="Fresh List" ID="ID_928929976" CREATED="1609990754285" MODIFIED="1609990759712">
<node TEXT="Set valued function" ID="ID_1431257568" CREATED="1609990760342" MODIFIED="1609990767070"/>
<node TEXT="proof carrying data structure" ID="ID_1418161020" CREATED="1609990772447" MODIFIED="1609990792611"/>
<node TEXT="Any" ID="ID_1141421059" CREATED="1609990819140" MODIFIED="1609990822050">
<node TEXT="here" ID="ID_1546836780" CREATED="1609991661319" MODIFIED="1609991663000"/>
<node TEXT="there" ID="ID_1162193758" CREATED="1609991663489" MODIFIED="1609991665378"/>
</node>
<node TEXT="insert" ID="ID_1479901665" CREATED="1609990795810" MODIFIED="1609990799803"/>
<node TEXT="insert / cons and Any" ID="ID_265930485" CREATED="1609990800355" MODIFIED="1609990813411"/>
<node TEXT="enumeration of pair" ID="ID_622029876" CREATED="1610006179353" MODIFIED="1610006194627"/>
</node>
<node TEXT="proofs" ID="ID_71982613" CREATED="1609990838839" MODIFIED="1609990843748">
<node TEXT="2" OBJECT="java.lang.Long|2" ID="ID_1357773799" CREATED="1609990844233" MODIFIED="1609990848197"/>
<node TEXT="3" OBJECT="java.lang.Long|3" ID="ID_285070989" CREATED="1609990848906" MODIFIED="1609990849643"/>
<node TEXT="5" OBJECT="java.lang.Long|5" ID="ID_553387365" CREATED="1609990862246" MODIFIED="1609990864317"/>
<node TEXT="4" OBJECT="java.lang.Long|4" ID="ID_922425691" CREATED="1609991325580" MODIFIED="1609991327765"/>
<node TEXT="5" OBJECT="java.lang.Long|5" ID="ID_884482373" CREATED="1609991337411" MODIFIED="1609991338693">
<node TEXT="compilation" ID="ID_1593187399" CREATED="1609991339281" MODIFIED="1609991342163"/>
</node>
</node>
<node TEXT="analysis" ID="ID_1668179685" CREATED="1609991697619" MODIFIED="1609991708118">
<node TEXT="overhead of proof carrying data structure" ID="ID_976735517" CREATED="1609991348749" MODIFIED="1609991361000">
<node TEXT="type" ID="ID_652487156" CREATED="1609991361589" MODIFIED="1609991365082"/>
<node TEXT="heap" ID="ID_876968413" CREATED="1609991365590" MODIFIED="1609991378981">
<node TEXT="product" ID="ID_198657579" CREATED="1609991379414" MODIFIED="1609991383275"/>
</node>
<node TEXT="type check" ID="ID_1804210435" CREATED="1609991389516" MODIFIED="1609991394532"/>
<node TEXT="compiled" ID="ID_1786891269" CREATED="1609991395061" MODIFIED="1609991405394"/>
</node>
<node TEXT="connection of computation and type" ID="ID_1028780772" CREATED="1609991716388" MODIFIED="1609991737610"/>
</node>
<node TEXT="appendix" ID="ID_1923999271" CREATED="1609991414119" MODIFIED="1609991419659">
<node TEXT="ZF fix" ID="ID_639095351" CREATED="1609991419999" MODIFIED="1609991498844">
<node TEXT="od max" ID="ID_882118125" CREATED="1609991570586" MODIFIED="1609991574172">
<node TEXT="Set and Class" ID="ID_785523216" CREATED="1609991576795" MODIFIED="1609991581126"/>
</node>
</node>
<node TEXT="next" ID="ID_987134788" CREATED="1609991499494" MODIFIED="1609991503587">
<node TEXT="tychonov" ID="ID_1788489591" CREATED="1609991504061" MODIFIED="1609991513116">
<node TEXT="topology" ID="ID_188550186" CREATED="1609991514960" MODIFIED="1609991518554"/>
</node>
<node TEXT="ZF" ID="ID_1650804627" CREATED="1609991556425" MODIFIED="1609991560227">
<node TEXT="cohen model" ID="ID_77996053" CREATED="1609991560836" MODIFIED="1609991563971"/>
</node>
</node>
</node>
</node>
<node TEXT="implementation" POSITION="left" ID="ID_1359586090" CREATED="1606377006821" MODIFIED="1606378512035">
<node TEXT="group" FOLDED="true" ID="ID_287565717" CREATED="1606377015762" MODIFIED="1606377020854">
<node TEXT="hierarchy" ID="ID_1217977502" CREATED="1606377891530" MODIFIED="1606377895546"/>
</node>
<node TEXT="permutation" FOLDED="true" ID="ID_618128777" CREATED="1606377021262" MODIFIED="1606377026259">
<node TEXT="bijection on Data.Fin" FOLDED="true" ID="ID_597466250" CREATED="1606377091642" MODIFIED="1606377110065">
<node TEXT="abstract" ID="ID_1158865640" CREATED="1606378591811" MODIFIED="1606378598578"/>
</node>
<node TEXT="combinator" FOLDED="true" ID="ID_1921597264" CREATED="1606377392195" MODIFIED="1606377397374">
<node TEXT="prep" ID="ID_330696821" CREATED="1606377397374" MODIFIED="1606377403998"/>
<node TEXT="swap" ID="ID_1228887457" CREATED="1606377426743" MODIFIED="1606377430099"/>
<node TEXT="pins" ID="ID_478525497" CREATED="1606377451571" MODIFIED="1606377453688"/>
<node TEXT="not unique" ID="ID_1582208431" CREATED="1606378599458" MODIFIED="1606378602838"/>
</node>
<node TEXT="List ℕ" FOLDED="true" ID="ID_447332615" CREATED="1606377147557" MODIFIED="1606377174712">
<node TEXT="not unique" ID="ID_608038587" CREATED="1606378608757" MODIFIED="1606378614329"/>
</node>
<node TEXT="FL n" FOLDED="true" ID="ID_1784079007" CREATED="1606377179308" MODIFIED="1606377183560">
<node TEXT="decremental Data.Fin List" FOLDED="true" ID="ID_1790506416" CREATED="1606377183560" MODIFIED="1606377199633">
<node TEXT="unique" ID="ID_665257211" CREATED="1606378617080" MODIFIED="1606378619230"/>
<node TEXT="1 to 1" ID="ID_1530010631" CREATED="1606378626590" MODIFIED="1606378628302"/>
</node>
<node TEXT="FL n to Perm" ID="ID_767155416" CREATED="1606377458903" MODIFIED="1606377465105"/>
<node TEXT="Perm to FL" ID="ID_135453080" CREATED="1606377465737" MODIFIED="1606377469086"/>
<node TEXT="iso" ID="ID_1105006832" CREATED="1606377470255" MODIFIED="1606377472861"/>
<node TEXT="injection" ID="ID_846590614" CREATED="1606377473713" MODIFIED="1606377475642"/>
</node>
<node TEXT="conversion" FOLDED="true" ID="ID_1747777855" CREATED="1606377382892" MODIFIED="1606377386415">
<node TEXT="direct refl" ID="ID_932941583" CREATED="1606727219039" MODIFIED="1606727227206"/>
</node>
</node>
<node TEXT="enumeration of permutation" FOLDED="true" ID="ID_1172252989" CREATED="1606377221243" MODIFIED="1606377228975">
<node TEXT="List" ID="ID_239078628" CREATED="1606377230408" MODIFIED="1606377235895"/>
<node TEXT="Fresh List" FOLDED="true" ID="ID_1866566989" CREATED="1606377236436" MODIFIED="1606377239550">
<node TEXT="term itself is simple" ID="ID_536448598" CREATED="1606378273582" MODIFIED="1606378282243"/>
<node TEXT="type is complicated" ID="ID_334436404" CREATED="1606378284710" MODIFIED="1606378294962"/>
</node>
</node>
<node TEXT="commutator" FOLDED="true" ID="ID_368973198" CREATED="1606377028929" MODIFIED="1606377032873">
<node TEXT="generator" FOLDED="true" ID="ID_134730969" CREATED="1606377252812" MODIFIED="1606377264147">
<node TEXT="not necessary" ID="ID_1941243109" CREATED="1606727532690" MODIFIED="1606727540677"/>
</node>
<node TEXT="cong" ID="ID_85252223" CREATED="1606377266582" MODIFIED="1606377272449"/>
</node>
<node TEXT="solvable" FOLDED="true" ID="ID_1847720925" CREATED="1606377033697" MODIFIED="1606377036804">
<node TEXT="second order" ID="ID_854168913" CREATED="1606377038096" MODIFIED="1606377049483"/>
<node TEXT="third order" FOLDED="true" ID="ID_795750040" CREATED="1606377050074" MODIFIED="1606377055050">
<node TEXT="a lof of easy equation" ID="ID_1251443358" CREATED="1606377679670" MODIFIED="1606377695159"/>
</node>
<node TEXT="forth order" FOLDED="true" ID="ID_128064534" CREATED="1606377055860" MODIFIED="1606377059872">
<node TEXT="too many" ID="ID_660493111" CREATED="1606377695633" MODIFIED="1606377699494"/>
<node TEXT="use Fresh list" ID="ID_1107095798" CREATED="1606377807636" MODIFIED="1606377814089"/>
</node>
<node TEXT="fifth order" FOLDED="true" ID="ID_1986356" CREATED="1606377067933" MODIFIED="1606377071318">
<node TEXT="5 contains 3" ID="ID_1761950431" CREATED="1606377814808" MODIFIED="1606377837816"/>
<node TEXT="in two different parts" ID="ID_649320127" CREATED="1606377838561" MODIFIED="1606377854524"/>
</node>
</node>
<node TEXT="solvable by Fresh List" FOLDED="true" ID="ID_1242936721" CREATED="1606377705411" MODIFIED="1606377721190">
<node TEXT="sorted" ID="ID_228290840" CREATED="1606377721190" MODIFIED="1606377724012"/>
<node TEXT="insert" ID="ID_55633177" CREATED="1606377861188" MODIFIED="1606377863199"/>
<node TEXT="any" FOLDED="true" ID="ID_1234121961" CREATED="1606377863601" MODIFIED="1606377865965">
<node TEXT="it contains everything?" ID="ID_1547561546" CREATED="1606377874500" MODIFIED="1606377881123"/>
</node>
</node>
<node TEXT="Equalizer" FOLDED="true" ID="ID_1439868847" CREATED="1606377291291" MODIFIED="1606377314716">
<node TEXT="equality on concrete object" ID="ID_503791605" CREATED="1606377314717" MODIFIED="1606377329048"/>
<node TEXT="equality on abstract object" ID="ID_1955667161" CREATED="1606377330172" MODIFIED="1606377336895"/>
</node>
</node>
<node TEXT="paper" POSITION="left" ID="ID_873264480" CREATED="1606378512784" MODIFIED="1606378523086">
<node TEXT="problem" FOLDED="true" ID="ID_696482092" CREATED="1606379096805" MODIFIED="1606379099309">
<node TEXT="enumerating commutator" ID="ID_752930881" CREATED="1606379099309" MODIFIED="1606379107094"/>
<node TEXT="is this really a proof?" ID="ID_1614555070" CREATED="1606379107643" MODIFIED="1606379117201"/>
<node TEXT="all connected in Agda" ID="ID_1678061189" CREATED="1606379124041" MODIFIED="1606379130309"/>
</node>
<node TEXT="Galois introduction" FOLDED="true" ID="ID_917416576" CREATED="1606378515709" MODIFIED="1606378542758">
<node TEXT="easy and quick" ID="ID_1764355857" CREATED="1606727909781" MODIFIED="1606727916012"/>
</node>
<node TEXT="Agda introduction" FOLDED="true" ID="ID_434512007" CREATED="1606378543316" MODIFIED="1606378547552">
<node TEXT="Group representation" ID="ID_762123734" CREATED="1606378554127" MODIFIED="1606378563015"/>
<node TEXT="Permutation" ID="ID_610013381" CREATED="1606378568196" MODIFIED="1606378572610"/>
</node>
<node TEXT="Representation of Permutation" ID="ID_1573892815" CREATED="1606378575594" MODIFIED="1606378585288">
<node TEXT="math" FOLDED="true" ID="ID_1797326547" CREATED="1606378644922" MODIFIED="1606378648975">
<node TEXT="abc" ID="ID_1052913615" CREATED="1606378648976" MODIFIED="1606378650331"/>
</node>
<node TEXT="list" FOLDED="true" ID="ID_1900422285" CREATED="1606378653895" MODIFIED="1606378655245">
<node TEXT="not unique" ID="ID_844966393" CREATED="1606378655246" MODIFIED="1606378658614"/>
<node TEXT="no permutation property" ID="ID_1727235552" CREATED="1606378668243" MODIFIED="1606378675693"/>
</node>
<node TEXT="bijection" FOLDED="true" ID="ID_1560893595" CREATED="1606378662595" MODIFIED="1606378666125">
<node TEXT="abstract" ID="ID_147732297" CREATED="1606378666126" MODIFIED="1606378695445"/>
</node>
<node TEXT="combinator" FOLDED="true" ID="ID_1561884094" CREATED="1606378701314" MODIFIED="1606378706107">
<node TEXT="not unique" ID="ID_560079212" CREATED="1606378706108" MODIFIED="1606378708991"/>
</node>
<node TEXT="FL" FOLDED="true" ID="ID_1817493034" CREATED="1606378715224" MODIFIED="1606378717668">
<node TEXT="unique" ID="ID_1607834497" CREATED="1606378717668" MODIFIED="1606378719860"/>
<node TEXT="1 to 1" ID="ID_1710096678" CREATED="1606378721382" MODIFIED="1606378723061"/>
</node>
</node>
<node TEXT="enumeration of FL" ID="ID_1432020010" CREATED="1606378927269" MODIFIED="1606378933032">
<node TEXT="Fresh List" ID="ID_124351974" CREATED="1606378933032" MODIFIED="1606378936038"/>
<node TEXT="Any" ID="ID_863395146" CREATED="1606378936579" MODIFIED="1606378938352"/>
</node>
<node TEXT="Solvable" FOLDED="true" ID="ID_115815719" CREATED="1606378586134" MODIFIED="1606378745085">
<node TEXT="Commutator" ID="ID_132480944" CREATED="1606378745085" MODIFIED="1606378748529"/>
<node TEXT="Commutator implementationn" ID="ID_326008986" CREATED="1606378750600" MODIFIED="1606378757686"/>
</node>
<node TEXT="proof os Solvability" ID="ID_1064018730" CREATED="1606378771575" MODIFIED="1606378780946">
<node TEXT="on abstract Permutation" FOLDED="true" ID="ID_679164783" CREATED="1606378780946" MODIFIED="1606378788919">
<node TEXT="on 2" ID="ID_1953177659" CREATED="1606378834624" MODIFIED="1606378835927"/>
</node>
<node TEXT="using FL" FOLDED="true" ID="ID_1180179827" CREATED="1606378791247" MODIFIED="1606378794009">
<node TEXT="on 3" ID="ID_1092149501" CREATED="1606378809099" MODIFIED="1606378817784"/>
<node TEXT="on 5" ID="ID_1783576565" CREATED="1606378818337" MODIFIED="1606378821442"/>
</node>
<node TEXT="using Fresh List" FOLDED="true" ID="ID_699752428" CREATED="1606378801731" MODIFIED="1606378808475">
<node TEXT="on 4" ID="ID_413592226" CREATED="1606378827030" MODIFIED="1606378829422"/>
</node>
</node>
<node TEXT="anaysis" FOLDED="true" ID="ID_1520622758" CREATED="1606378844704" MODIFIED="1606378848322">
<node TEXT="computation time" FOLDED="true" ID="ID_471167918" CREATED="1606378848322" MODIFIED="1606378857868">
<node TEXT="overhead" ID="ID_1271917563" CREATED="1606728089529" MODIFIED="1606728094180"/>
</node>
<node TEXT="static and dynamic" ID="ID_913962071" CREATED="1606378865355" MODIFIED="1606378869923"/>
<node TEXT="abstract and concrete" ID="ID_1135285650" CREATED="1606378872154" MODIFIED="1606378879318"/>
<node TEXT="data type with proof" ID="ID_615335887" CREATED="1606378885692" MODIFIED="1606378890266"/>
<node TEXT="agda programming tech" ID="ID_490445683" CREATED="1606727991341" MODIFIED="1606728003312"/>
</node>
</node>
</node>
</map>