<<<<<<< working copy
Thu May 17 15:26:56 JST 2018

    findNode -> replaceNode -> getRedBlackTree だが

        findNode -> P0 -> replaceNode -> P1 -> getRedBlackTree 

   という形で証明しても良い。一挙に証明するのは,可能だろうけど、良くないはず。

||||||| base
=======


>>>>>>> destination
Sun May  6 17:54:50 JST 2018

    do1 a $ \b ->  do2 b next を、do1 と do2  に分離することはできる?


Mon Apr 30 17:15:16 JST 2018

    Stack の初期化を別にするだけだと、置き換えの条件に到達した時に、Stack が empty になるのを保証できない
    やはり、 Stack + Current Tree = Original Tree という不変式を入れないとだめらしい

Mon Mar 26 17:43:06 JST 2018

    Decidable を使って Compare の場合分けを行う    
    Decidable を使うと Eq から x ≡ y の証明を取り出すことができる
    場合分けには Trichotomous を使う
    compareTri を完成させる    Done

Fri Jan  5 16:43:26 JST 2018

    unbalanced binary search tree の動作を調べる

    RedBlackTree の put を完成させる

    RedBlackTree の Deletion を完成させる

                 unbalanced binary search tree と同様の動作をする

                  木の深さの最小と最大の差が２倍を超えない

    CodeGear/DataGear が構成する圏を定義する

    goto を定義して meta 計算を可能にする

    DataSegment をすべて含む sum 型を定義しmetaDataSegmentとする

    実行環境をcontextとして定義しgotoと合わせて並列実行をモデル化する

    Monad の合成に必要な規則を上の圏上に定義する

    synchronizedQueue の仕様をCTLを使って定義する

    Gearsで記述したsynchornizedQueueを検証する

    gotoを用いてモデル検査と証明の組み合わせを実現する

    
Wed Aug 27 17:52:00 JST 2019

    別で定義した TriCotomos や \=? などの Relation の関数を
    Agdaで定義してあるものに置き換える,まとめる
    
    HoareLogic をベースにした SingleLinkedStack の作成
    
    HoareLogic ベースの Tree の証明