------------------------------------------------------------------------------ ( n : Nat ! data (---------! where (------------! ; !-------------! ! Nat : * ) ! zero : Nat ) ! suc n : Nat ) ------------------------------------------------------------------------------ data (-----------! where lt : Order ; eq : Order ; gt : Order ! Order : * ) ------------------------------------------------------------------------------ ( m, n : Nat ! let !-----------------------! ! compareTo m n : Order ) compareTo m n <= rec m { compareTo m n <= case m { compareTo zero n <= case n { compareTo zero zero => eq compareTo zero (suc n) => lt } compareTo (suc m) n <= case n { compareTo (suc m) zero => eq compareTo (suc m) (suc n) => lt } } } ------------------------------------------------------------------------------ data (---------! where (-----------! ; (-------------! ! Col : * ) ! red : Col ) ! black : Col ) ------------------------------------------------------------------------------ ( f : Col ; n : Nat ! data !--------------------! ! Tree f n : * ) ( al : Tree black n ! ( al : Tree f n ! ! ! ! ! ! x : Nat ! ! x : Nat ! ! ! ! ! ! ar : Tree black n ! ! ar : Tree g n ! where (--------------! ; !-------------------! ; !----------------! ! leaf : ! ! redN al x ar ! ! blackN al x ar ! ! Tree black ! ! : Tree red n ) ! : Tree black ! ! % zero ) ! % (suc n) ) ------------------------------------------------------------------------------ data (---------! where (------------! ; (-------------! ! Way : * ) ! left : Way ) ! right : Way ) ------------------------------------------------------------------------------ ( sf : Col ; sn : Nat ; tf : Col ; tn : Nat ! data !----------------------------------------------! ! TZ sf sn tf tn : * ) where (-------------------! ! root : TZ f n f n ) ( w : Way ; a : Tree black n ; x : Nat ; z : TZ red n rf rn ! !--------------------------------------------------------------! ! inRed w a x z : TZ black n rf rn ) ( w : Way ; a : Tree f n ; x : Nat ; z : TZ black (suc n) rf rn ! !------------------------------------------------------------------! ! inBlack w a x z : TZ hf n rf rn ) ------------------------------------------------------------------------------ ( t : Tree hf hn ; z : TZ hf hn rf rn ! let !--------------------------------------! ! plug t z : Tree rf rn ) plug t z <= rec z { plug t z <= case z { plug t root => t plug t (inRed w a x z) <= case w { plug t (inRed left a x z) => plug (redN t x a) z plug t (inRed right a x z) => plug (redN a x t) z } plug t (inBlack w a x z) <= case w { plug t (inBlack left a x z) => plug (blackN t x a) z plug t (inBlack right a x z) => plug (blackN a x t) z } } } ------------------------------------------------------------------------------ ( x : Nat ! ! ! ! w : Way ! ! ! ( f : Col ! ! pr : Tree red n ! ! ! ( a : ! ! ! ! n : Nat ! ! Tree f n ! ! pb : Tree black n ! data !----------! where !-------------! ; !-------------------! ! Prob f n ! ! level f a ! ! panic x w pr pb ! ! : * ) ! : Prob g n ) ! : Prob red n ) ------------------------------------------------------------------------------ ( p : Prob hf hn ; z : TZ hf hn rf rn ! let !--------------------------------------! ! solve p z : Prob rf rn ) solve p z <= rec z { solve p z <= case z { solve p root => p solve p (inRed w a x z) <= case p { solve (level f a) (inRed w a' x z) <= case f { solve (level red a) (inRed w a' x z) => solve (panic x w a a') z solve (level black a) (inRed w a' x z) <= case w { solve (level black a) (inRed left a' x z) => solve (level ? (redN a x a')) z solve (level black a) (inRed right a' x z) => solve (level ? (redN a' x a)) z } } } solve p (inBlack w a x z) <= case p { solve (level f a) (inBlack w a' x z) <= case w { solve (level f a) (inBlack left a' x z) => solve (level ? (blackN a x a')) z solve (level f a) (inBlack right a' x z) => solve (level ? (blackN a' x a)) z } solve (panic p w pr pb) (inBlack w' a x z) <= case pr { solve (panic p w (redN prl x prr) pb) (inBlack w' a x' z) <= case w { solve (panic p left (redN prl x prr) pb) (inBlack w' a x' z) <= case w' { solve (panic p left (redN prl x prr) pb) % (inBlack left a x' z) => solve (level ? (redN (blackN prl x prr) p!! z ! !% (blackN pb x' a) )) solve (panic p left (redN prl x prr) pb) % (inBlack right a x' z) => solve (level ? (redN (blackN a p prl) x!! z ! !% (blackN prr x' pb) )) } solve (panic p right (redN prl x prr) pb) (inBlack w' a x' z) <= case w' { solve (panic p right (redN prl x prr) pb) % (inBlack left a x' z) => solve (level ? (redN (blackN pb p prl) x!! z ! !% (blackN prr x' a) )) solve (panic p right (redN prl x prr) pb) % (inBlack right a x' z) => solve (level ? (redN (blackN a x' pb) p!! z ! !% (blackN prl x prr) )) } } } } } } ------------------------------------------------------------------------------