def invalid_valid_tail

qasim-bend-kit@0.1.0.2 · proof/JSON_NumberLexProof.bend:83

import Base
import qasim-bend-kit@0.1.0.2/libs/JSON.bend as J
import qasim-bend-kit@0.1.0.2/proof/JSON_PrimitiveProof.bend as P

83def invalid_valid_tail(+tail: String,
84                       +state: J.NumberState,
85                       +character: Char,
86                       other: {J.number_char(character) == J.NOther{} : J.NumberChar},
87                       evidence: {J.number_valid_end(J.number_valid_step(SCon{character, tail}, state)) == True{} : Bool}) -> Empty:
88    false_true(Equal.trans(Bool, False{},
89        J.number_valid_end(J.number_valid_step(tail, J.NumberInvalid{})), True{},
90        Equal.sym(Bool, J.number_valid_end(J.number_valid_step(tail, J.NumberInvalid{})), False{}, P.invalid_end(tail)),
91        Equal.trans(Bool,
92            J.number_valid_end(J.number_valid_step(tail, J.NumberInvalid{})),
93            J.number_valid_end(J.number_valid_step(tail, J.number_next(state, character))), True{},
94            Equal.sym(Bool,
95                J.number_valid_end(J.number_valid_step(tail, J.number_next(state, character))),
96                J.number_valid_end(J.number_valid_step(tail, J.NumberInvalid{})),
97                Equal.cong(J.NumberState, Bool, s => J.number_valid_end(J.number_valid_step(tail, s)),
98                    J.number_next(state, character), J.NumberInvalid{}, number_next_other(character, state, other))),
99            number_valid_cons(character, tail, state, evidence))))