list.bend checks

The empty list is a right identity for append: xs ++ [] = xs.

The empty list is a left identity for append: [] ++ xs = xs.

Append is associative: (xs ++ ys) ++ zs = xs ++ (ys ++ zs).

The length of an append is the sum of the lengths.

The reverse accumulator loop appends the reversed list to the accumulator.

Reversing an append reverses and swaps the parts: reverse (xs ++ ys) = reverse ys ++ reverse xs.

Reversing twice gives the list back.

Reversing preserves the length.

A right fold over an append folds the first part onto the fold of the second.

Taking n elements and appending the rest after dropping n gives the list back.

Mapping preserves the length.

Mapping over an append maps each part: map f (xs ++ ys) = map f xs ++ map f ys.

Mapping twice is mapping the composition: map g (map f xs) = map (g . f) xs.

Taking zero elements gives the empty list.

Dropping zero elements gives the list back.

Taking from the empty list gives the empty list.

Dropping from the empty list gives the empty list.

Taking n elements leaves min(n, length) of them.

Dropping n elements leaves length - n of them.

Taking as many elements as the list has gives the list back.

Dropping as many elements as the list has gives the empty list.

Taking m from the first n is taking min(n, m).

Dropping m after dropping n is dropping n + m.

Reversing the empty list gives the empty list.

Reversing a one-element list gives it back.

Replicating x n times gives a list of length n.

Range(n) has length n.

Zipping two lists gives the length of the shorter one.

Appending after a cons: (x :: xs) ++ ys = x :: (xs ++ ys).

The empty list has length zero.

A cons is one longer than its tail.

Concatenating an append concatenates each part: concat (xss ++ yss) = concat xss ++ concat yss.

A left fold over an append folds the second part from the fold of the first.

Mapping commutes with reversing: map f (reverse xs) = reverse (map f xs).

All over an append is all over each part, joined by and.

Any over an append is any over each part, joined by or.

Filtering an append filters each part.

An append contains x iff either part does.

Filtering never makes a list longer.

The head of a cons is a member of it.

Membership is preserved when a new head is prepended.

Nothing is a member of the empty list.

Membership on the left of an append.

Membership on the right of an append.

The empty list is sorted by any comparator.

A singleton list is sorted by any comparator.

A sorted tail with an in-order head is sorted.

The head pair of a sorted cons-cons list is in order.

The tail of a sorted cons-cons list is sorted.

A sorted list has a sorted tail.

The empty list is a right identity for append: xs ++ [] = xs, reversed to rewrite toward the simple side.

The empty list is a left identity for append: [] ++ xs = xs, reversed to rewrite toward the simple side.

Append is associative: (xs ++ ys) ++ zs = xs ++ (ys ++ zs), reversed to rewrite toward the simple side.

The length of an append is the sum of the lengths, reversed to rewrite toward the simple side.

The reverse accumulator loop appends the reversed list to the accumulator, reversed to rewrite toward the simple side.

Reversing an append reverses and swaps the parts: reverse (xs ++ ys) = reverse ys ++ reverse xs, reversed to rewrite toward the simple side.

Reversing twice gives the list back, reversed to rewrite toward the simple side.

Reversing preserves the length, reversed to rewrite toward the simple side.

A right fold over an append folds the first part onto the fold of the second, reversed to rewrite toward the simple side.

Taking n elements and appending the rest after dropping n gives the list back, reversed to rewrite toward the simple side.

Mapping preserves the length, reversed to rewrite toward the simple side.

Mapping over an append maps each part: map f (xs ++ ys) = map f xs ++ map f ys, reversed to rewrite toward the simple side.

Mapping twice is mapping the composition: map g (map f xs) = map (g . f) xs, reversed to rewrite toward the simple side.

Taking zero elements gives the empty list, reversed to rewrite toward the simple side.

Dropping zero elements gives the list back, reversed to rewrite toward the simple side.

Taking from the empty list gives the empty list, reversed to rewrite toward the simple side.

Dropping from the empty list gives the empty list, reversed to rewrite toward the simple side.

Taking n elements leaves min(n, length) of them, reversed to rewrite toward the simple side.

Dropping n elements leaves length - n of them, reversed to rewrite toward the simple side.

Taking as many elements as the list has gives the list back, reversed to rewrite toward the simple side.

Dropping as many elements as the list has gives the empty list, reversed to rewrite toward the simple side.

Taking m from the first n is taking min(n, m), reversed to rewrite toward the simple side.

Dropping m after dropping n is dropping n + m, reversed to rewrite toward the simple side.

Reversing the empty list gives the empty list, reversed to rewrite toward the simple side.

Reversing a one-element list gives it back, reversed to rewrite toward the simple side.

Replicating x n times gives a list of length n, reversed to rewrite toward the simple side.

Range(n) has length n, reversed to rewrite toward the simple side.

Zipping two lists gives the length of the shorter one, reversed to rewrite toward the simple side.

Appending after a cons: (x :: xs) ++ ys = x :: (xs ++ ys), reversed to rewrite toward the simple side.

The empty list has length zero, reversed to rewrite toward the simple side.

A cons is one longer than its tail, reversed to rewrite toward the simple side.

Concatenating an append concatenates each part: concat (xss ++ yss) = concat xss ++ concat yss, reversed to rewrite toward the simple side.

A left fold over an append folds the second part from the fold of the first, reversed to rewrite toward the simple side.

Mapping commutes with reversing: map f (reverse xs) = reverse (map f xs), reversed to rewrite toward the simple side.

All over an append is all over each part, joined by and, reversed to rewrite toward the simple side.

Any over an append is any over each part, joined by or, reversed to rewrite toward the simple side.

Filtering an append filters each part, reversed to rewrite toward the simple side.

An append contains x iff either part does, reversed to rewrite toward the simple side.

Filtering never makes a list longer, reversed to rewrite toward the simple side.

Membership in a list, as a reusable proposition.

A list is sorted by a comparator when every adjacent pair is in order.