kdrag.notation.induct_seq

kdrag.notation.induct_seq(a: SeqRef, P) → Proof

>>> x = smt.Const("x", smt.SeqSort(smt.IntSort()))
>>> induct(x, lambda s: smt.Length(s) >= 0)
|= Implies(And(Length(Empty(Seq(Int))) >= 0,
            ForAll(z!..., Length(Unit(z!...)) >= 0),
            ForAll([x!..., y!...],
                   Implies(And(Length(x!...) >= 0,
                               Length(y!...) >= 0),
                           Length(Concat(x!..., y!...)) >= 0))),
        Length(x) >= 0)

Parameters:

a (SeqRef)

Return type:

Proof