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'