module Meas where import LiquidPrelude X1:[a] -> {V:Int | (0 <= V),(V = len([X1]))}mylen [] = x:Int# -> {V:Int | (V = x)}0 mylen (_:xs) = x:Int# -> {V:Int | (V = x)}1 x:Int -> y:Int -> {V:Int | (V = (x + y))}`plus` X1:[a] -> {V:Int | (0 <= V),(V = len([X1]))}mylen {V:[a] | (V = xs)}xs (a -> b) -> X1:[a] -> {V:[b] | (len([V]) = len([X1]))}mymap a -> bf [] = forall a. {V:[a] | (nully([V]) = 0),(len([V]) = 0)}[] mymap f (x:xs) = a(a -> bf ax) forall a. a -> ys:[a] -> {V:[a] | (nully([V]) = 1),(len([V]) = (1 + len([ys])))}: ((a -> b) -> X1:[a] -> {V:[b] | (len([V]) = len([X1]))}mymap a -> bf {V:[a] | (V = xs)}xs) forall a. lq:[a] -> [a]myrev = {V:[a] | true,(V = X1)}go forall a. {V:[a] | (nully([V]) = 0),(len([V]) = 0)}[] where acc:[a] -> X1:[a] -> {V:[a] | (len([V]) = (len([acc]) + len([X1]))), (len([V]) = (len([X1]) + len([acc])))}go [a]acc (x:xs) = acc:[a] -> X1:[a] -> {V:[a] | (len([V]) = (len([acc]) + len([X1]))), (len([V]) = (len([X1]) + len([acc])))}go (axforall a. a -> ys:[a] -> {V:[a] | (nully([V]) = 1),(len([V]) = (1 + len([ys])))}:{V:[a] | true,(V = acc)}acc) {V:[a] | (V = xs)}xs go acc [] = {V:[a] | true,(V = acc)}acc X1:[a] -> ys:[a] -> {V:[a] | (len([V]) = (len([X1]) + len([ys]))), (len([V]) = (len([ys]) + len([X1])))}myapp [] [a]ys = {V:[a] | true,(V = ys)}ys myapp (x:xs) ys = axforall a. a -> ys:[a] -> {V:[a] | (nully([V]) = 1),(len([V]) = (1 + len([ys])))}:(X1:[a] -> ys:[a] -> {V:[a] | (len([V]) = (len([X1]) + len([ys]))), (len([V]) = (len([ys]) + len([X1])))}myapp {V:[a] | (V = xs)}xs {V:[a] | true,(V = ys)}ys) zs :: [Int] [{V:Int | (0 <= V)}]zs = forall a. ??? -> a -> a -> [a][x:Int# -> {V:Int | (V = x)}1..x:Int# -> {V:Int | (V = x)}100] zs' :: [Int] [{V:Int | (X1 <= V),(0 <= V),(X1 < V)}]zs' = forall a. ??? -> a -> a -> [a][x:Int# -> {V:Int | (V = x)}500..x:Int# -> {V:Int | (V = x)}1000] Boolprop2 = x:{V:Bool | (TAG([V]) = True)} -> {V:Bool | (V = x)}assert ({V:Int | (V = len([zs])),(0 <= V)}n1 x:Int -> y:Int -> {V:Bool | ((TAG([V]) = True) <=> (x = y))}`eq` n2) where n1 = forall a. lq:[a] -> {V:Int | (0 <= V)}mylen {V:[{V:Int | (0 <= V)}] | (V = zs)}zs n2 = forall a. lq:[a] -> {V:Int | (0 <= V)}mylen forall a b. (a -> b) -> a -> b$ forall a b. (a -> b) -> lq:[a] -> [b]mymap (x:Int -> y:Int -> {V:Int | (V = (x + y))}`plus` x:Int# -> {V:Int | (V = x)}1) {V:[{V:Int | (0 <= V)}] | (V = zs)}zs Boolprop3 = x:{V:Bool | (TAG([V]) = True)} -> {V:Bool | (V = x)}assert ({V:Int | (V = len([zs])),(0 <= V)}n1 x:Int -> y:Int -> {V:Bool | ((TAG([V]) = True) <=> (x = y))}`eq` n2) where n1 = forall a. lq:[a] -> {V:Int | (0 <= V)}mylen {V:[{V:Int | (0 <= V)}] | (V = zs)}zs n2 = forall a. lq:[a] -> {V:Int | (0 <= V)}mylen forall a b. (a -> b) -> a -> b$ forall a. lq:[a] -> [a]myrev {V:[{V:Int | (0 <= V)}] | (V = zs)}zs Boolprop4 = x:{V:Bool | (TAG([V]) = True)} -> {V:Bool | (V = x)}assert (Int({V:Int | (V = len([zs])),(0 <= V)}n1 x:Int -> y:Int -> {V:Int | (V = (x + y))}`plus` n2) x:Int -> y:Int -> {V:Bool | ((TAG([V]) = True) <=> (x = y))}`eq` n3) where n1 = forall a. lq:[a] -> {V:Int | (0 <= V)}mylen {V:[{V:Int | (0 <= V)}] | (V = zs)}zs n2 = forall a. lq:[a] -> {V:Int | (0 <= V)}mylen {V:[{V:Int | (X1 <= V),(0 <= V),(X1 < V)}] | (V = zs')}zs' n3 = forall a. lq:[a] -> {V:Int | (0 <= V)}mylen forall a b. (a -> b) -> a -> b$ forall a. lq:[a] -> lq:[a] -> [a]myapp {V:[{V:Int | (0 <= V)}] | (V = zs)}zs {V:[{V:Int | (X1 <= V),(0 <= V),(X1 < V)}] | (V = zs')}zs'