kdrag.theories.seq.induct_list

kdrag.theories.seq.induct_list(x: SeqRef, P)

>>> x = smt.Const("x", Seq(smt.IntSort()))
>>> P = smt.Function("P", Seq(smt.IntSort()), smt.BoolSort())
>>> induct_list(x, P)
|= Implies(And(P(Empty(Seq(Int))),
            ForAll([hd!..., tl!...],
                  Implies(P(tl!...),
                          P(Concat(Unit(hd!...), tl!...))))),
        P(x))

Parameters:

x (SeqRef)