Prove that a list whose sum is greater than its length must have at least one element greater than one

test_list_elt_gt_1.py

from z3 import *

def test_list_elt_gt_1():
  ll = Datatype('ll')
  ll.declare('empty')
  ll.declare('cons', ('car', IntSort()), ('cdr', ll))
  ll = ll.create()
  list_sum = Function('list_sum', ll, IntSort(), BoolSort())
  list_len = Function('list_len', ll, IntSort(), BoolSort())
  a,e = Consts('a e', ll)
  b,c,d = Ints('b c d')
  
  fp = Fixedpoint()
  fp.declare_var(a,b,c,d,e)
  fp.register_relation(list_sum, list_len)
  fp.rule(list_sum(a, 0), a == ll.empty)
  fp.rule(list_sum(a, d), [a != ll.empty, b < 1, ll.cons(b, e) == a, list_sum(e, c), b + c == d])
  fp.rule(list_len(a, 0), a == ll.empty)
  fp.rule(list_len(a, d), [a != ll.empty, b < 1, ll.cons(b, e) == a, list_len(e, c), 1 + c == d])
  assert fp.query(And(list_sum(a, b), list_len(a, c), a != ll.empty, b >= c)) == unsat
  assert fp.query(And(list_sum(a, b), list_len(a, c), a != ll.empty, b < c)) == sat