JSONNumberLexProof.invalid_valid_tail: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend as JSONNumberLexProof
Lines 83-99 of qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend&start_line=83&end_line=99

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

def invalid_valid_tail(+tail: String,
                       +state: J.NumberState,
                       +character: Char,
                       other: {J.number_char(character) == J.NOther{} : J.NumberChar},
                       evidence: {J.number_valid_end(J.number_valid_step(SCon{character, tail}, state)) == True{} : Bool}) -> Empty:
    false_true(Equal.trans(Bool, False{},
        J.number_valid_end(J.number_valid_step(tail, J.NumberInvalid{})), True{},
        Equal.sym(Bool, J.number_valid_end(J.number_valid_step(tail, J.NumberInvalid{})), False{}, P.invalid_end(tail)),
        Equal.trans(Bool,
            J.number_valid_end(J.number_valid_step(tail, J.NumberInvalid{})),
            J.number_valid_end(J.number_valid_step(tail, J.number_next(state, character))), True{},
            Equal.sym(Bool,
                J.number_valid_end(J.number_valid_step(tail, J.number_next(state, character))),
                J.number_valid_end(J.number_valid_step(tail, J.NumberInvalid{})),
                Equal.cong(J.NumberState, Bool, s => J.number_valid_end(J.number_valid_step(tail, s)),
                    J.number_next(state, character), J.NumberInvalid{}, number_next_other(character, state, other))),
            number_valid_cons(character, tail, state, evidence))))

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Char
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=NumberChar
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=NumberState
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=number_char
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=number_next
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=number_valid_end
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=number_valid_step
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend&name=false_true
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend&name=number_next_other
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_NumberLexProof.bend&name=number_valid_cons
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_PrimitiveProof.bend&name=invalid_end