IMPS: An Interactive Mathematical Proof System

Theories

• abelian-groups
• arithmetic-mod-5
• arithmetic-mod-n
• bird
• commutative-monoid-theory
• complete-ordered-field
• complete-partial-order
• counting-theorem-theory
• csm-0-theory
• csm-theory
• data-theory
• datagrams
• degree-equivalence
• det-hoare-machines
• det-state-machines
• directed-monoid-theory
• family-indicators
• fields
• filtered-networks
• fixed-interval-theory
• fixed-interval-theory
• fts+invariant
• fts-theory
• generic-tcp-theory
• generic-theory-1
• generic-theory-2
• generic-theory-3
• generic-theory-4
• geometry-1
• geometry-1
• geometry-2
• geometry-2
• geometry-3
• geometry-4
• geometry-5
• graphs
• group-actions
• groups
• groups
• h-o-real-arithmetic
• hoare-machines
• indicator-pairs
• indicators
• interval-in-cpo
• lct-theory
• linear-order
• machine-arithmetic
• mappings-from-an-interval
• mappings-from-an-interval-to-a-normed-space
• mappings-from-an-interval-with-endpoints-to-a-normed-space
• mappings-into-a-partial-order
• mappings-into-a-pointed-metric-space
• memory-objects
• metric-spaces
• monoid-theory
• monoid-transition-system
• monoids-with-index-set
• ms-closed-ball
• ms-subspace
• networks
• normed-groups
• normed-linear-spaces
• octets
• one-route-networks
• op-semantics
• ordered-field
• packet-trajectory-theory
• partial-order
• places
• pointed-metric-spaces
• pointed-ms-2-tuples
• port-theory
• pre-networks
• pre-octets
• protocol-theory
• pure-generic-theory-0
• pure-generic-theory-1
• pure-generic-theory-1-with-1-subsort
• pure-generic-theory-2
• pure-generic-theory-2-with-1-subsort
• pure-generic-theory-2-with-2-subsorts
• pure-generic-theory-3
• pure-generic-theory-3-with-2-subsorts
• pure-generic-theory-4
• relational-theory
• routed-networks
• schroeder-bernstein-theory
• sequences
• sexpression
• single-filter-theory
• state-machines
• stevens
• three-place-predicate-theory
• ultrametric-spaces
• vector-spaces

• Translations

• act->conjugate
• act->left%trans
• act->left-mul
• act->right%trans
• act->right-mul
• act->set%conjugate
• commutative-monoid-theory-to-multiplicative-mod-n
• commutative-monoid-theory-to-multiplicative-rr
• complete-order-reverse
• complete-ordered-field-interpretable
• complete-partial-order-to-generic-theory-1
• complete-partial-order-to-h-o-real-arithmetic
• complete-partial-order-to-h-o-real-arithmetic-reverse
• cpo-to-fixed-interval-theory
• external-smtp
• fields-to-rr
• fields-to-rr-extended
• finite-specialization-of-rgm
• generic-theory-1-to-geometry
• generic-theory-1-to-packet-trajectory
• generic-theory-2-to-indicator-pairs
• generic-theory-to-directed-monoid
• group-to-field-multiplicative-group
• groups->subgroup
• groups-to-multiplicative-kk
• h-o-real-arithmetic-instantiation
• ind_1->pp
• ind_1-to-sexp
• ind_2-to-place
• index-families
• index-on-zz
• index-on-zz-reverse
• iterate->three-place-predicate
• lct-interpretation
• left%trans<->right%trans
• linear-order-reverse
• mapint-to-mapint-normed-space
• mappings-from-an-interval-to-ns-extension-specialization
• mappings-on-interval-into-ns-to-rr
• mappings-pointed-metric-spaces-2-tuples
• monoid-transition-system-to-directed-monoid-theory
• monoids-to-groups
• ms-subspace-to-ms-closed-ball
• ms-to-ms-closed-ball
• mul-reverse
• normed-spaces-to-rr
• order-reverse
• packet-trajectory-theory-to-filtered-networks
• places-to-memory
• rel-to-coll
• relativize-to-interval
• reverse-filter
• schroeder-bernstein->generic-theory-2
• schroeder-bernstein-symmetry
• seq->bird
• sequences->hoare-actions
• subspaces-to-function-subspace
• subspaces-to-uc-function-subspace
• the-kernel-translation
• ultrametric-to-degree-equivalence
• ultrametric-to-degree-equivalence

• Theorems

• <-translated
• <-translated-reverse
• <=-characterization
• <=-translated
• *_ext-totality
• *_mod-characterization
• *_mod-identity
• *_mod-total
• +_mod-characterization
• +_mod-identity
• +_mod-total
• -_mod-computation-non-zero
• -_mod-computation-zero
• 0-characterization
• 0-multiple-is-group-identity
• 0-times-is-0
• 1-multiple-is-element
• 1-not-negative
• 1-positive
• 1stnsquares
• 3rd-mersenne-number-is-prime
• a%copy-definedness
• a%cosets%sort-members-are-in-a%cosets
• a%cosets-are-equinumerous
• a%cosets-contains-a
• a%cosets-has-positive-f-card
• a%cosets-have-equal-f-card
• a%cosets-is-a-partition-of-ab
• a%cosets-is-total
• a%even-a%inf-disjoint
• a%even-a%odd-a%inf-cover-dom-of-f
• a%even-a%odd-disjoint
• a%f-induction
• a%f-induction-bi
• a%f-induction-conv
• a%odd-a%inf-disjoint
• a%seq-b%seq-hierarchies-lemma
• a%seq-hierarchy
• a%seq-to-b%seq-step-by-f
• a-contains-e
• a-has-positive-f-card
• a-is-a-subgroup
• a-is-defined-in-a%cosets%sort
• a-point-separates-a-line-not-both
• a-point-separates-a-line-or
• a-seq-b-seq-definedness
• a-seq-definedness
• a-singleton-containing-a-particular-element
• abs-free-characterization-of-real-limit
• absolute-value-absolute-value
• absolute-value-inversion
• absolute-value-non-negative
• absolute-value-non-positive
• absolute-value-product
• absolute-value-quotient
• absolute-value-zero
• abstr-is-total
• abstract-bolzano-weierstrass
• abstract-intermediate-value
• accept
• accepted%actions-is-complement-of-refused%actions
• accepted%transitions-characterization-of-<_must%refuse
• accepted%transitions-is-prefix-closed
• accepted%transitions_ff-is-support
• accessible%from+tr
• accessible%from-cases
• accessible%from-initial-equals-accessible
• accessible%from-initial-is-accessible
• accessible%from-preserves-accessible
• accessible%from-reflexive
• accessible%from-transitivity
• accessible-states-accessible%from-initial
• act-associativity
• act-id
• act-is-total
• act_ff-is-act
• action-by-stabilizer-member
• action-macete
• action-representatives-can-have-norm-le-1
• aix
• all-failures-are-total
• alternate-iota-free-characterization-of-sep%deg
• alternate-uniqueness-for-pairs
• anti-cyclic
• anti-cyclic
• append-agrees-with-first-below-length
• append-cons
• append-cons-not-fseq
• append-fseq-implies-first-fseq
• append-fseq-implies-second-fseq
• append-fseq-macete
• append-is-fseq
• append-is-nil-implies-left-is-nil
• append-shifts-second-arg
• append_to_netstate-is-defined-in-netstates
• append_to_netstate-is-total
• append_to_state-is-defined-in-states
• append_to_state-is-total
• approx-existence
• approx-monotonicity
• approx-reflexivity
• approx-separation
• approx-symmetry
• approx-transitivity
• archimedean
• associative-law-for-multiplication
• associative-law-for-multiplication-for-fields
• associative-law-for-multiplication-for-monoids
• associative-law-for-multiplication-for-monoids
• associative-law-for-multiplication-pre-reals
• associativity-of-composition
• associativity-of-logand
• associativity-of-logxor
• at-least-two-points
• at-least-two-points
• atom-1
• atom-128
• atom-16
• atom-2
• atom-32
• atom-4
• atom-64
• atom-8
• b%inf-subseteq-of-ran-of-f
• b%odd-subseteq-of-ran-of-f
• b%sort-members-are-in-b
• b-contains-e
• b-is-a-subgroup
• b-is-lct%gg%subgroup
• b-is-total
• b-seq-definedness
• ball-definedness
• ball-membership-condition
• base-types
• bb-sort-characterization
• bernoullis-inequality
• bet(a,m,p)
• between-implies-collinear-contra
• bfun-ball-closure
• bfun-ball-closure-corollary
• bfun-ball-membership-lemma
• bfun-completeness
• bfun-values-defined-lemma
• bifurcate->=-inequality
• bifurcate-<=-inequality
• bifurcate-product->-inequality
• bifurcate-product->=-inequality
• bifurcate-product-<-inequality
• bifurcate-product-<=-inequality
• bifurcate-product-equation
• big-intersection-member
• big-union-member
• big-union-recursion
• biiterate-invariance
• biiterate-recursive-unfolding
• biiterate-switch
• biiterate-undefined-for-negative
• bijectiveness-of-omega%embedding-at-finite-set
• binary-int-function-lemma
• binomial-expansion-lemma
• binomial-theorem
• bound%place%monotonicty
• bound%place%stability
• bound%place-abstr-definedness
• bound%place-characterization
• bound%place-contains-dom-gamma
• bound%place-invariance
• bound%place-totality
• bounded%non%decreasing%seq-convergent
• bounded%nonincreasing%seq-convergent
• bounded-bfun%dist
• br%partial%trans%closure-is-total
• br%partial%trans%closure-lemma-1
• br%partial%trans%closure-lemma-2
• br%partial%trans%closure-total-aux
• c%copy-definedness
• c%fill-no-op
• c%redirect-no-op
• cancel
• cancel-pre-reals
• car-cdr-same-domain
• car-iterate-defined-lemma
• car-pair-rewrite
• cardinality-3
• cardinality-at-least-2
• cardinality-at-least-2-lemma
• cardinality-at-least-3-lemma
• cardinality-at-most-1-lemma
• cardinality-definedness-lemma
• cardinality-of-a-finite-zeta-orbit
• cardinality-of-connecting%lines-bound
• cardinality-of-intervals-lemma
• cardinality-of-zeta-orbit
• cardinality-reduction
• case-1-mach-copy
• case-1-mach-copy-thm
• case-2-mach-copy-thm
• case-3-mach-copy-thm
• cauchy-characterization-for-sep%dist
• cauchy-double-index-characterization
• cauchy-extends
• cauchy-implies-discrete%lim-is-lim
• cauchy-ptwise-converge-implies-uniform-convergence
• cauchy-ultrametric-condition
• cdr-nulle-undefined
• cdr-pair-rewrite
• characterization-of-<_must%refuse
• characterization-of-closure
• characterization-of-closure-lemma-1
• characterization-of-closure-lemma-2
• characterization-of-contractiveness
• characterization-of-derivative
• characterization-of-divisibility
• characterization-of-equivalence-predicates
• characterization-of-gcd
• characterization-of-limit
• characterization-of-monoid%prod%unordered
• characterization-of-non-expansiveness
• characterization-of-omega-embedding
• characterization-of-omega-embedding-for-finite-sets
• characterization-of-omega-embedding-for-infinite-sets
• characterization-of-omega-embedding-lemma
• characterization-of-primitive
• characterization-of-real-limit
• characterization-ultrametric-limit-of-fns
• closed-balls-are-closed
• closed-balls-are-defined
• closure-contains-set
• closure-under-unions-with-finite-sets
• coll%closed-closed-under-le
• coll%closed-iff-fixed-under-coll%closure
• coll%closure-exists
• coll%closure-of-pair
• coll-conjunctive-permuter
• coll-disjunctive-permuter
• coll-disjunctive-permuter
• collapse-invariance-condition
• collapse-of-finite-is-finite-lemma
• collinear-all-cases
• collinear-all-cases
• collinear-flipper-1-2
• collinear-flipper-1-2
• collinear-flipper-1-3
• collinear-flipper-1-3
• collinear-flipper-2-3
• collinear-flipper-2-3
• collinear-implies-distinct
• collinear-implies-distinct-lemma
• com_kk-definedness
• comb-0-value-lemma
• comb-1-value-lemma
• comb-definedness-lemma
• comb-ident
• comb-integrality-lemma
• comb-is-a-comb_kk
• comb-m-value-lemma
• comb-reduction-schema
• comb_kk-0-value-lemma
• comb_kk-ident
• comb_kk-m-value-lemma
• comb_kk-null-lemma
• comb_kk-second-null-lemma
• combination-decomposition
• combination-disjointness
• combination-reduction
• combinations-card
• commutative-law-for-monoids
• commutative-law-for-multiplication
• commutative-law-for-multiplication-for-fields
• commutative-law-for-multiplication-pre-reals
• commutative-law-stack-lemma
• complete-implies-bicomplete
• complete-induction
• complete-induction-schema
• complete-induction-schema
• completeness
• completeness-extends
• completeness-of-ff
• completeness-of-total%fns
• composition-decreases-domain
• composition-decreases-range
• composition-of-continuous-is-continuous
• composition-of-continuous-special-case
• composition-with-id-left
• composition-with-id-right
• composition-with-total-id-left
• composition-with-total-id-right
• compositionality-of-omega-embedding
• condition-for-contractions-on-function-spaces
• congruence-characterization
• congruence-reflexive
• congruence-symmetric
• congruence-transitive
• connecting%lines-of-finite-sets-are-finite
• connecting-line-sufficient-condition
• cons-append
• cons-car-cdr
• cons-car-cdr-lemma
• cons-fseq-implies-fseq
• cons-is-fseq
• cons-to-nil-is-fseq
• constant-function-lemma
• constant-function-lipschitz-characterization
• constant-is-continuous
• constant-on-subintervals
• constant-on-subintervals-corollary
• constant-uniformly-continuous
• constants
• constrict-of-finite-sequence-is-finite-sequence
• contains-an-element-implies-non-empty
• continuity-is-closed-under-uniform-limits
• continuity-of-dist-expression
• continuous%bfun%complete
• continuous-at-point-defined
• contraction-characterization-for-sep%dist
• contractive-mapping-fixed-point-theorem
• convergence-test-for-complete-spaces
• convergent%to%infinity-linear-form
• convergent-implies-cauchy
• converse-sm-induction
• copy-definedness
• copy-fn-dom-bound
• copy-liveness
• copy-liveness-corollary
• copy-safety
• cut-interval-at-left
• decreasing-property-of-sup-tail
• decremented-partition-lemma
• default-c%copy-bound%place
• default-c%copy-lower
• default-c%copy-un-bound%place
• default-in-bound-place-implies-bound
• default-modification-lemma
• default-multiplicity-reduction
• defined-iota-expression
• defined-iota-expression-elimination
• defined-iota-expression-existence
• defined-iota-expression-full-existence
• defined-iota-expression-iota-free-uniqueness
• defined-iota-expression-satisfiability
• defined-iota-expression-uniqueness
• defined-nth%root-is-nonnegative
• defined-nth%root-is-nonnegative
• definedness-of-dangling-conditionals
• definedness-of-discrete%lim
• definedness-of-generator
• definedness-of-le
• definedness-of-mu-for-contractions
• definedness-of-mu-for-contractions-on-functions
• definedness-of-sep%deg
• definedness-of-set%min
• delivery-transition
• delta-step-is-a-step-fn
• deny_all_module-correctness
• deriv-of-constant
• deriv_r-restricts-deriv-lemma
• derivative-at-point-bound-lemma
• derivative-bound-lemma
• derivative-of-a-linear-map
• det-fun-sm-thm
• det-state%histories-extensible-1
• diff-conditionally-one-to-one
• diff-conditionally-onto
• diff-union-equal-whole
• diff-with-indic-is-disj-from-indic
• difference-conjunction-conversion
• difference-of-a-disjoint-union
• difference-of-a-union
• difference-of-disjoint-sets
• diffuse_comb
• direct-image-disjointness-conversion
• direct-image-subset-conversion
• directed-property
• discrete%lim-eventually-constant-property
• discrete-sets-contain-inf
• discrete-sets-contain-sup
• discrete-sets-contain-sup-lemma
• disj-commutativity
• dist-continuity-lemma
• dist-uniformly-continuous
• distinctness-1-2
• distinctness-1-2
• distinctness-1-3
• distinctness-1-3
• distinctness-2-3
• distinctness-2-3
• div-by-zero-undefined-pre-reals
• div-by-zero-undefined-pre-reals
• divides-implies-le
• divisibility
• divisibility-by-prime
• divisibility-characterization-of-generator
• divisibility-is-transitive
• divisibility-lemma
• divisibility-preserves-ideal-membership
• division-characterization-fields
• division-characterization-pre-reals
• division-in-terms-of-exponential
• division-non-zero
• division-of-fractions
• division-of-fractions-2
• division-with-remainder
• dom-of-an-indicator
• dom-of-h
• dom-of-id
• dom-of-inverse
• dom-of-omega%embedding-at-finite-set
• dom-ran-disjointness-lemma
• domain-composition
• domain-membership-iff-defined
• domain-of-a-bijective-composition
• domain-of-a-restriction
• domain-of-almost-total-map
• domain-of-exponentiation
• domain-of-fct-mapping
• domain-of-flow%ext-lemma
• domain-of-inverse
• domain-of-omega-embedding-for-finite-sets
• domain-of-omega-embedding-for-infinite-sets
• domain-of-quotient
• domain-of-total-map
• drop-all
• drop-all-or-more
• drop-cons
• drop-from-nil
• drop-is-fseq
• drop-of-append
• drop-sequence-lemma
• drop-some-from-append
• dseq-definedness
• dseq-distance-bound
• dseq-distance-bound-corollary
• dseq-quasi-invariance
• dsm-induction-biconditional
• dsm-induction-biconditional-conv
• e-behaves-as-identity
• e-is-never-refused
• edges-have-two-endpoints
• element-of-a-subset-is-an-element
• elements-of-host_router-domain-are-disjoint
• embeds-equinumerous-transitivity
• embeds-implies-equinumerous-to-subset
• embeds-in-empty-indic
• embeds-is-reflexive
• embeds-is-transitive
• empty-indic-has-f-card-zero
• empty-indic-has-f-card-zero-rewrite
• empty-indic-sup-is-undefined
• empty-inters-iff-disjoint
• empty-segment-lemma
• empty_indic-is-empty
• empty_state-is-a-filtered-state
• empty_state-is-a-state
• emptyset-equals-its-coll%closure
• emptyset-is-coll%closed
• endpoint-ordering
• endpoints-is-total
• entry%index-characterization
• entry%index-definedness
• eps-delta-characterization-of-continuity
• equal-actions-iff-equal-right-trans
• equal-actions-implies-equal-right-trans
• equal-arguments-implies-equal
• equal-iota-expressions
• equal-iota-expressions-lemma
• equal-right-trans-implies-equal-actions
• equality-of-conditional-term
• equality-of-conditional-term-backwards
• equality-of-fractions
• equals-empty-indic-iff-empty
• equals-implies-equinumerous
• equinumerous-embeds-transitivity
• equinumerous-finite-cardinals
• equinumerous-finite-cardinals-lemma-1
• equinumerous-finite-cardinals-lemma-2
• equinumerous-finite-cardinals-lemma-3
• equinumerous-finite-cardinals-lemma-3a
• equinumerous-finite-cardinals-lemma-3b
• equinumerous-finite-cardinals-lemma-4
• equinumerous-finite-cardinals-lemma-5
• equinumerous-finite-cardinals-lemma-6
• equinumerous-implies-embeds
• equinumerous-implies-f-card-quasi-equal
• equinumerous-is-reflexive
• equinumerous-is-symmetric
• equinumerous-is-transitive
• equinumerous-to-empty-indic
• equiv-reflexivity
• equiv-symmetry
• equiv-transitivity
• ethernet1
• even-and-odd-natural-numbers-are-disjoint
• even-iff-suc-is-odd
• every-direction-is-inbound-or-outbound
• every-non-trivial-ideal-contains-a-positive-element
• example-op
• example-op-1
• existence-left
• existence-left
• existence-middle
• existence-middle
• existence-of-derivative
• existence-of-limit
• existence-of-prime-factorization
• existence-of-real-limit
• existence-right
• existence-right
• existential-cons-car-cdr
• exp-out
• expansion-lemma
• exponent-defined-lemma-0
• exponent-defined-lemma-1
• exponent-distributes-over-product
• exponent-distributes-over-product-corollary
• exponent-distributes-over-product-lemma-0
• exponent-distributes-over-product-lemma-1
• exponent-domain
• exponent-non-zero-lemma-0
• exponent-non-zero-lemma-1
• exponent-of-inverse
• exponent-of-inverse-corollary
• exponent-of-inverse-lemma
• exponential-monotonicity-lemma
• exponential-of-0
• exponential-of-0-corollary
• exponential-of-0-lemma-1
• exponential-of-0-lemma-2
• exponential-of-1-corollary
• exponential-of-1-lemma
• exponential-of-1-lemma-0
• exponentiation-of-fractions-lemma
• exponents-of-fractions
• extending
• extending-collinear-sets
• external%smpt%filter%module-correctness
• external-and-internal-are-disjoint
• external-multiplication-conversion
• f-card-disjoint-union
• f-card-disjoint-union-lemma-1
• f-card-disjoint-union-lemma-2
• f-card-disjoint-union-lemma-3
• f-card-equal-iff-finite-and-equinumerous
• f-card-equal-implies-equinumerous
• f-card-leq-iff-finite-and-embeds
• f-card-of-a-finite-cardinal
• f-card-of-b
• f-card-of-lct%orbit-at-a
• f-card-of-lct%stabilizer-at-a
• f-card-zero-partition-lemma
• f-injectiveness
• f-totality
• f_card_difference
• f_card_difference
• f_seq_q-characterization
• factor-groups-are-groups
• factorial-definedness
• factorial-non-zero
• factorial-non-zero-1
• factorial-of-zero
• factorial-out
• factorization-of-act
• failed-delivery-transition
• failure-alt-failure-equivalence
• failure-non-empty-condition
• failure-property
• failure_q-is-closed-under-lim
• failures-characterization-of-<_may%refuse
• failures-characterization-of-=%may%refuse
• failures-characterization-of-eqv%may%refuse
• false%val-is-false
• false%val-is-not-true
• ff%dist-is-bounded
• ff-completeness
• field-zero-is-not-field-one
• filtered-states-exist
• filtered_states-are-closed-under-takefirst
• filtered_states-defining-axiom-lemma
• finite-and-equinumerous-implies-f-card-equal
• finite-cardinal-application
• finite-cardinal-is-f-indic
• finite-cardinal-members-are-<
• finite-closure-under-singleton-lemma
• finite-non-extendable-sets-may-be-refused
• finite-sets-have-maximal-elements
• finite-sets-have-maximum-elements
• finite-sets-have-minimal-elements
• finite-sets-have-minimum-elements
• finite-sets-in-nn-are-bounded
• finite-uniform-partition-lemma
• finite-uniform-partition-theorem
• finitely-many-on%connecting%line
• finitely-many-on%connecting%line%through
• finiteness-of-a
• finiteness-of-a%cosets
• finiteness-of-a-inters-b
• finiteness-of-a-partition
• finiteness-of-a-partition-lemma
• finiteness-of-ab
• finiteness-of-b
• finiteness-of-lct%gg%subgroup
• finiteness-of-orbits
• finiteness-of-stabilizers
• finiteness-of-subgroups
• finiteness-of-zeta-orbit
• finiteness-of-zeta-stabilizer
• first%entry-characterization
• first%entry-definedness
• first%entry-definedness
• first%entry-equation
• first%entry-identity-in-set
• first%entry-iteration
• first%entry-iteration
• first%entry-locality
• first%entry-minimality
• first%entry-restricted-invariance
• first%entry-restriction-lemma
• first%entry-restriction-lemma-2
• first-datagram-in-tcp_connection-lemma
• first-defined-entails-pair
• first-of-a-pair-is-defined
• first-projection
• floor-below-arg
• floor-characterization
• floor-definedness
• floor-inequality-characterization
• floor-not-much-below-arg
• floor-plus-1-exceeds-arg
• flow%ext-complement-invariance
• flow%ext-definedness
• flow%ext-domain-monotonicity
• flow%ext-extension-theorem-1
• flow%ext-extension-theorem-2
• flow%ext-extension-theorem-3
• flow%ext-idempotency
• flow%ext-minimality
• flow%ext-minimality-lemma
• flow%ext-recursive-equation
• flow%ext-restricted-invariance
• flow%ext-restricted-invariance
• flow%ext-restriction-lemma
• fn%approx-existence
• fn%approx-monotonicity
• fn%approx-reflexivity
• fn%approx-separation
• fn%approx-symmetry
• fn%approx-transitivity
• fn%dist-is-bounded
• fn%dist-non-negative
• fn%dist-reflexive
• fn%dist-small-distance-chracterization
• fn%dist-symmetric
• fn%dist-triangle-inequality
• forwarding-transition
• fts+init-secure
• fts+next-secure
• fts+secure
• fun-sec
• fundamental-counting-theorem
• fundamental-sm-thm
• fundamental-theorem-of-calculus
• g%h%ok-corollary
• g%h%ok-dom-g-disj-dom-h
• g%h%ok-dom-g-unbound
• g%h%ok-dom-h-disj-dom-g
• g%h%ok_2-disjointness
• g%h%ok_2-etc-implies-bound
• g%h%ok_2-iota-definedness
• g-injectiveness
• g-totality
• gamma-c%copy-unchanged
• gcd-for-zero
• gcd-is-gcd-of-absolute-value
• gcd-of-multiple
• gcd-of-negative
• gcd-usually-is-non-zero
• gcd_ma-restricts-gcd
• gcd_rho-defined-for-nonnegative-args
• gcd_rho-is-gcd
• general-commutative-law
• general-commutative-law-corollary
• general-commutative-law-corollary-1
• general-commutative-law-corollary-2
• general-commutative-law-induction-step-lemma
• general-composition-of-continuous-functions
• general-induction
• generalized-combinatorial-identity
• generalized-triangle-inequality
• generic_tcp_filter_module-correctness
• geometric-series-formula
• geometric-series-is-summable%nonnegative
• geometric-series-upper-estimate
• geometric-series-upper-estimate-lemma
• germ-equality-condition
• gg-is-a-subgroup
• group-commutativity
• group-to-field-multiplicative-group-obl-1
• group-to-field-multiplicative-group-obl-2
• group-to-field-multiplicative-group-obl-3
• group-to-field-multiplicative-group-obl-4
• group-to-field-multiplicative-group-obl-5
• groups->subgroup-obl-1
• groups->subgroup-obl-2
• h%ok-implies-dom-unbound
• h-accessible-lemma
• h-bijectiveness
• h-histories-defined-at-0
• h-histories-defined-at-state-predecessor
• h-histories-defined-on-action-segment
• h-histories-defined-on-state-segment
• h-histories-defined-on-state-segment-nn
• h-history-at-0-is-initial
• h-initial-implies-accessible
• h-injectiveness
• h-injectiveness-lemma
• h-next-preserves-accessible
• h-run-next
• h-run-run
• h-run-run-lemma
• h-sm-induction-forward
• h-surjectiveness
• h-tr-preserves-accessible
• hdsm-induction-biconditional-conv
• hereditary-property
• histories-defined-at-0
• histories-defined-on-action-segment
• histories-defined-on-state-segment
• histories-extensible
• history-action-length
• history-state-length
• homogeneity-of-deriv
• homogeneity-of-integral
• homogeneity-of-real-limit
• homogeneity-of-real-limit-corollary
• host-of-out_iface
• host-spnet-inversion
• host_router-is-total
• hosts-are-self-connected
• hsm-induction
• hsm-induction-biconditional
• id-is-injective-on-dom
• idempotence-of-subgroups
• identity-uniformly-continuous
• iface-is-an-iface-of-host
• iface_in_to_out-macete
• iface_out_to_in-macete
• iface_router-is-total
• ifill-abstraction
• ifill-definedness
• image-contained-in-range
• image-is-monotone-wrt-subseteq
• image-of-a%even-under-f
• image-of-a%inf-under-f
• image-of-a%odd-under-inverse-of-g
• image-of-a-finite-set-is-finite
• image-of-a-restriction
• image-of-domain-is-range
• image-subset-of-range-characterization
• image-under-inverse-of-injective-mapping
• implication-equivalent
• in-range-condition
• in-singleton-iff-equals-single-member
• in_seq-car
• in_seq-cdr
• in_seq-nil
• inbound
• inbound-filtering-transition
• independent%rules-dependent-condition
• independent%rules-independent-condition
• index-of-normalizer
• index-of-set-normalizer
• indic-free-characterization-of-dom
• indic-free-characterization-of-ran
• induct
• induction-in-cpos
• induction-pre-reals
• induction-principle-for-cpos
• inequality-2
• inf-defined-implies-non-empty
• inf-lemma
• inf-plus-epsilon
• inf-plus-epsilon-corollary
• infinite-append
• infinity-of-primes
• init%eqv-reflexive-property
• init%eqv-symmetric-property
• init%eqv-transitive-property
• initial-implies-accessible
• injective-and-surjective-is-total
• injective-composition
• injective-iff-injective-on-domain
• injective-implies-injective-on
• injectiveness-of-fct-mapping
• injectiveness-of-omega%embedding
• injectivity-of-a-restriction
• injectivity-of-trace
• int-division-lemma
• int-minus-lemma
• int-mod-lemma
• integer-combinations-form-an-ideal
• integer-exponent
• integer-exponent-lemma
• integer-exponentiation-definedness
• integer-exponentiation-definedness-dr
• integrability-condition
• integrable-implies-integral-exists
• integrable-implies-integral-is-continuous
• integral-of-a-constant
• integral-on-null-interval-is-zero
• interfaces-exist
• intermediate-value-theorem
• intersecting-balls-are-comparable
• intersection-commutativity
• intersection-conjunction-conversion
• intersection-of-les-with-common-first-point
• intersection-of-two-les
• intersection-of-two-lines
• interval-bounding-lemma
• interval-bounding-lemma
• interval-characterization
• interval-characterization
• interval-characterization
• interval-multiplicativity
• inv-is-total
• inv-is-total
• inv-of-e
• inv-of-inv
• invariance-composition
• invariance-of-ball
• invariance-of-gcd
• invariance-of-gcd-special-case
• inverse-composes-to-id
• inverse-composition-image-lemma
• inverse-defined-only-in-range
• inverse-defined-only-in-range-existential
• inverse-defined-within-range
• inverse-image-inters-preservation
• inverse-image-of-covers
• inverse-image-of-finite-covers
• inverse-image-union-preservation
• inverse-inverse-is-restriction
• inverse-is-a-left-inverse
• inverse-is-a-left-inverse-applied
• inverse-is-a-right-inverse
• inverse-is-a-right-inverse-applied
• inverse-is-injective
• inverse-of-inverse
• inverse-of-product
• inverse-range-only-in-domain
• inverse-range-within-domain
• inverse-replacement
• iota-free-characterization-of-after_ff
• iota-free-characterization-of-generator
• iota-free-characterization-of-mu
• iota-free-characterization-of-nth%root
• iota-free-characterization-of-prec%sup
• iota-free-characterization-of-prec%sup-existence
• iota-free-characterization-of-rel%closure
• iota-free-characterization-of-rlim
• iota-free-characterization-of-sep%deg
• iota-free-characterization-of-set%min
• iota-free-characterization-of-sexp%length
• iota-free-characterization-of-trace%on%line
• iota-free-definition-of-f-card
• iota-free-definition-of-f-indic-q
• iota-free-definition-of-length
• iota-free-definition-of-length-conv
• iota-free-smallest%proper%factor
• irreflexivity
• is-pair-implies-non-empty
• is-singleton-implies-non-empty
• is-triple-implies-non-empty
• istore-abstraction
• istore-is-ifill-followed-by-istore%simple
• iterate-definedness
• iterate-definedness-refinement
• iterate-definedness-refinement
• iterate-front-back-lemma
• iterate-front-back-lemma
• iterate-invariance
• iterate-locality
• iterate-restriction-lemma-1
• iterate-restriction-lemma-2
• iterate-sequence-converges
• iterate-totality
• iterate-translate
• iterated-distance-bound
• iterated-exponentiation-definability
• iterated-exponentiation-definability-corollary
• iterated-exponentiation-value
• iterated-exponentiation-value-corollary
• iterated-exponentiation-value-lemma-0
• iterated-exponentiation-value-lemma-1
• iterated-exponentiation-value-lemma-2
• iterated-nth%root
• knaster-fixed-point-theorem
• knaster-fixed-point-theorem-corollary
• lagranges-theorem
• last%a%index-to-last%b%index-step-by-f
• last-of-append-single
• lct%orbit-of-a-is-a%cosets
• lct%stabilizer-of-a-is-a-inters-b
• lct-obligation-1
• lct-obligation-2
• lct-obligation-3
• lct-obligation-4
• lct-obligation-5
• lct-obligation-6
• le-contains-left-point
• le-equality-condition
• le-equals-its-coll%closure
• le-is-a-line
• le-is-coll%closed
• le-is-collinear
• le-is-symmetric
• left%trans->right%trans-obligation
• left%trans-associativity
• left%trans-is-total
• left%trans-right%trans-associativity
• left-act-inv
• left-cancellation-law
• left-cancellation-law-for-monoids
• left-denominator-removal-for-equalities
• left-denominator-removal-for-inequalities
• left-denominator-removal-for-strict-inequalities
• left-distributive-law
• left-distributive-law-for-fields
• left-distributive-law-pre-reals
• left-group-equation
• left-inv-cancellation
• left-iota-expression-equation-elimination
• left-left%trans-inv
• left-mul-id
• left-mul-inv
• left-mul-macete
• left-multiplicative-identity-for-monoids
• left-right%trans-inv
• left-translation-macete
• left-trivial-cancellation-law-left
• left-trivial-cancellation-law-right
• length-0-implies-nil
• length-characterizes-definedness
• length-existence-implies-uniqueness
• length-non-negative
• length-non-negative
• length-of-append
• length-of-append-quasi-eq
• length-of-collapse-lemma
• length-of-cons
• length-of-cons-alt
• length-of-cons-alt-1
• length-of-constrict-of-finite-sequence
• length-of-drop
• length-of-drop-one
• length-of-pre-cons
• length-of-product
• length-of-takefirst
• les-are-connecting-lines
• lim%rr-negative
• lim%rr-preserves-lower-bound
• lim%rr-preserves-upper-bound
• lim-characterization-for-sep%dist
• lim-preservation
• lim-preservation-global
• limit-definedness-extends
• limit-depends-on-tail
• limit-of-constants
• limit-of-subsequence
• limit-of-subsequence-corollary
• limit-translation-invariance
• line-intersects-at-most-two-sides-of-a-triangle-lemma-1
• lines-are-infinite
• lines-are-le
• lines-contain-two-points
• lines-exist
• lipschitz%bound%on%subsets
• lipschitz%bound%on-extends
• lipschitz%bound-translation-inversion
• lipschitz-bound-is-continuous
• lipschitz-bound-is-total
• lipschitz-bound-is-uniformly-continuous
• lipschitz-on-interval-characterization
• list-characterization
• list-totality
• little-counting-theorem
• lngth-of-e
• local-context-introduction-for-monoid-prod
• locality-for-monoid-prod
• locality-of-derivative
• locality-of-flow%ext
• locality-of-flow%ext-corollary
• locality-of-integrals
• locality-of-integrals-lemma
• locally-lipschitz-implies-lipschitz
• locally-lipschitz-implies-lipschitz-plus
• logand-is-idempotent
• logand-is-total
• logand-simplification-lemma-1
• logxor-is-total
• loopback_spnet-gives-a-loopback-spnet
• loopback_spnet-gives-spnet-with-a-single-host
• loopback_spnet-host
• loopback_spnet-is-bijective
• loopback_spnet-is-total
• lower-definedness
• lower-for-bound-place
• lower-for-unbound-place
• lower-h%plus
• lower-is-c%copy%fn
• lower-semicontinuity-of-continuous
• lub-property-of-prec%sup
• make-tex-correspondence
• map-append
• map-cons
• map-distributes-over-composition
• map-f-is-total
• map-inverse
• map-inverse-1
• map-means-compose
• map-through-nil
• map-totality
• max%on%set-bigger-than-members
• max-lemma
• maximal-is-maximum
• maximum-1st-arg
• maximum-2nd-arg
• maxint-division-lemma
• maxint-is-positive
• maxint-pos-mod-lemma
• may%accept%after-negation-of-must%refuse%after
• mean-value-theorem
• mean-value-theorem-corollary-0
• mean-value-theorem-corollary-1
• mean-value-theorem-for-integrals
• mean-value-theorem-for-integrals-preliminary-form
• mean-value-theorem-on-subintervals
• mean-value-theorem-on-subintervals-corollary
• meaning-of-indic-from-pred-element
• meaning-of-indic-from-sort-element
• meaning-of-inverse-image-membership
• meaning-of-length
• meaning-of-length-rev
• meaning-of-zero
• membership-in-a-domain
• membership-in-a-range
• membership-in-diff
• membership-in-intersection
• membership-in-union
• metric-separation
• metric-separation-for-reals
• min-definedness
• min-lemma
• min-under-nondecreasing-fn-lemma
• minimal-is-minimum
• minimum-1st-arg
• minimum-2nd-arg
• minint-division-lemma
• minint-is-negative
• minint-is-negative-maxint
• minint-pos-mod-lemma
• minorizes-property-of-prec%sup
• mod-characterization
• mod-n-range-in-zz_mod
• mod-of-integer-is-integer
• mod-of-negative
• modular-value
• monoid%prod-distributes-over-**
• monoid-identity-behaves-as-identity
• monoid-null-prod
• monoid-operation-behaves-as-composition
• monoid-permutation-theorem
• monoid-prod-out
• monoid-triv-prod
• monotone-fixed-point-theorem
• monotone-product-lemma
• monotonicity-for-multiplication
• monotonicity-for-sum
• monotonicity-of-coll%closure
• monotonicity-of-exponentiation
• monotonicity-of-floor
• monotonicity-of-inverse
• monotonicity-of-nth%root
• monotonicity-of-omega%embedding
• monotonicity-of-prec%sup
• monotonicity-of-prec%sup-of-range
• monotonicity-of-sb-functional
• monotonicity-of-span
• ms-constant-continuous
• mul-associativity
• mul-is-total
• mult_mod-associative
• mult_mod-associative-lemma-1
• mult_mod-associative-lemma-2
• multiple-commutes-with-negation
• multiple-commutes-with-negation-corollary
• multiple-commutes-with-negation-in-group
• multiple-difference-lemma
• multiple-is-homogenuous
• multiple-of-group-identity
• multiple-totality
• multiple-totality-with-range
• multiplication-by-a-constant-is-continuous
• multiplication-congruence-invariance-lemma
• multiplication-of-fractions
• multiplication-of-fractions-left
• multiplication-of-fractions-right
• multiplication-preserves-divisibility
• multiplicative-identity
• multiplicative-identity-for-fields
• multiplicative-identity-pre-reals
• multiplicative-inverse-for-fields
• must%accept%after-negation-of-may%refuse%after
• must%refuse%after-characterization
• must%refuse%after-characterization-lemma
• nat-number-leq-iff-finite-cardinal-embeds
• natural-numbers-are-even-or-odd
• negated-defined-iota-expression-elimination
• negated-defined-iota-expression-elimination-1
• negated-defined-iota-expression-elimination-2
• negative-characterization-pre-reals
• negative-exponent-law
• negative-exponent-replacement
• negative-one-characterization
• negative-replacement
• negative-times-negative
• negativity-for-products
• nesting
• nesting-2
• netstates-exist
• next-accessible%from
• next-accessible%from-1
• next-definedness-condition
• next-for-discrete-sets
• next-preserves-accessible
• next_hop_iface-lemma
• nil-is-fseq
• no-factors-base
• no-factors-recursion
• no-units
• no_spoofing_module-correctness
• non-collinear
• non-collinear-2
• non-collinear-2-other
• non-collinear-between
• non-collinear-left
• non-collinear-right
• non-degeneracy
• non-degeneracy
• non-divisibility-into-1
• non-empty-range
• non-equality-1
• non-negativity-of-absolute-value
• non-negativity-of-distance
• non-nil-fseq-defined-at-0
• non-o_kk-is-closed-under-*_kk
• non-o_kk-is-closed-under-inv
• non-triviality
• non-vacuous
• non-zero-product
• nondecreasing%sums
• nondecreasing-sequences-converge
• nondecreasing-sequences-converge-corollary
• nonempty-a
• nonempty-b
• norm-continuity-lemma
• norm-scalar-multiplication
• norm-totality
• norm-totality
• norm-triangle-inequality
• norm-triangle-inequality
• norm-zero
• norm-zero
• normal-iff-conjugates-property
• normal-iff-cosets-property
• normal-implies-cosets-property
• not-everything-is-a-failure
• not-in-range-condition
• ns-multiple-of-continuous-is-continuous
• ns-sum-of-continuous-is-continuous
• ns-vector-multiple-of-continuous-is-continuous
• nth%cdr-list
• nth%root%existence
• nth%root-non-negative
• nth%root-of-zero
• nth%root-positive-for-positive
• nth%root-power
• nth-root-is-multiplicative
• nth-roots-are-unique
• nth-roots-exist
• null_state_condition-is-always-true
• nulle-is-not-pair
• nullified-monoid%prod-lemma
• nullify%incrementally
• o_kk-exponent
• o_kk-times-is-o_kk
• octet%lt-irreflexivity
• octet%lt-transitivity
• octet%lt-trichotomy
• octet%to%nn-is-injective
• octet-decomposition
• octet-unit-decomposition
• odd-iff-suc-is-even
• omega%embedding-at-finite-set-lemma
• omega%embedding-at-nonempty-indic
• omega%embedding-defined-at-zero
• omega%embedding-definedness
• omega%embedding-id-condition
• omega%embedding-is-total
• omega%embedding-strong-definedness
• omega%embedding-strong-definedness-lemma
• omega-0-is-empty-indicator
• omega-1-is-singleton
• omega-is-total
• omega-n-as-domain-lemma
• omega-of-successor
• on%connecting%line%through-characterization
• on%connecting%line-characterization
• one-exponent
• open-ball-definedness
• open-ball-membership-condition
• open-balls-are-defined
• open-balls-are-open
• open-mapping
• open-mapping-lemma
• opposite_direction-is-total
• orbit-is-total
• order-discreteness
• order-discreteness-pre-reals
• other-extending
• other-nesting
• other-point-lemma
• other-switching
• other-switching
• out_iface-is-an-interface-of-host
• outbound-filtering-transition
• overlapping-right-cosets
• pair-car-cdr
• pair-first-second
• pair-first-second-rewrite
• pair-totality
• pairs-are-collinear
• pairs-are-pairs
• pairs-are-pairs-rewrite
• parametrized-completeness
• parametrized-condition-for-contractions-on-function-spaces-lemma
• parametrized-definedness-of-mu-for-contractions
• parametrized-definedness-of-mu-for-contractions-lemma
• piecewise-integrable-is-integrable
• plus_mod-associative
• plus_mod-associative-lemma-1
• plus_mod-associative-lemma-2
• point-separation-for-distance
• point-separation-for-distance
• point-separation-for-rr-distance
• positive-f-card-iff-nonempty
• positive-prime-characterization
• positive-rational-characterization
• positivity-for-products
• positivity-for-products-of-negatives
• positivity-for-products-pre-reals
• positivity-for-r^n
• positivity-for-squares
• positivity-of-distance
• positivity-of-distance
• positivity-of-ff%dist
• positivity-of-inverse
• positivity-of-norm
• positivity-of-norm
• positivity-of-r
• positivity-of-rr-distance
• posrat%exp-characterization
• posrat%exp-definedness
• posrat%exp-iterated-exponent-property
• posrat%exp-multiplicative-property
• posrat%exp-nonnegative
• power-card
• power-decomposition
• power-disjointness
• power-fn-is-monotone
• power-fn-is-weakly%lipschitz
• power-reduction
• powers-arbitrarily-small
• prec%lim%inf-existence
• prec%lim%inf-lower-bound
• prec%lim%inf-upper-bound
• prec%majorizes%characterization
• prec%majorizes-property-of-prec%sup
• prec%sup-defined
• prec%sup-dominates-values
• prec-anti-symmetry
• prec-completeness
• prec-reflexivity
• prec-transitivity
• preceding-defined
• preceding-for-discrete-sets
• prefix-has-smaller-length-lemma
• prefix-is-reflexive
• prefix-is-transitive
• primality-test-refinement
• primality-test-refinement-lemma
• prime-divisor-of-a-general-product
• prime-divisor-of-a-power
• prime-divisor-of-a-prime
• prime-divisor-of-a-product
• primes-exist
• primitive-existence
• princ%ideal-contains-its-generator
• princ%ideal-is-ideal
• principal-ideal-theorem
• prod-decomposition
• prod-definedness
• prod-definedness-converse
• prod-integer-definedness
• prod-non-zero
• product-division-interchange
• product-gte-1
• product-in-terms-of-squares-lemma
• product-in-terms-of-squares-lemma
• product-is-divisible-by-factors
• product-of-continous-is-continuous
• product-of-fractions-lemma
• product-power-is-iterated-power
• proper-generator
• ptwise-closure-condition
• ptwise-continuity-is-closed-under-uniform-limits
• push-inv
• qq-*-closed
• qq-+-closed
• qq-^-closed
• qq-div-closed
• qq-minus-closed
• qq-sub-closed
• quotient-map-for-equivalence-relations
• r^n-convergent-to-infinity
• raise-condition
• raise-condition-corollary
• raise-condition-variant
• raise-condition-variant-1
• raise-lower-composition
• raise-totality
• ran-of-f-is-b%seq-at-1
• ran-of-h
• ran-of-h-lemma-1
• ran-of-h-lemma-2
• ran-of-h-lemma-3
• ran-of-id
• ran-of-inverse
• ran-of-omega%embedding
• ran-of-omega%embedding-is-subset
• ran-of-omega%embedding-lemma
• ran-of-omega%embedding-lemma-1
• ran-of-omega%embedding-lemma-2
• ran-of-omega%embedding-lemma-3
• ran-of-omega%embedding-lemma-4
• ran-of-omega%embedding-lemma-5
• range-composition
• range-domain-membership
• range-of-a-bijective-composition
• range-of-bijection-on-singleton
• range-of-failures
• range-of-fct-mapping
• rangenet-disjointness
• rangenet-is-total
• rational-power-lemma-1
• rational-power-lemma-2
• rational-power-lemma-3
• real-convergent-bounded
• real-limit-product
• real-limit-square
• real-limit-square-corollary
• refused%actions-is-total
• regular%place-characterization
• rel%closed-iff-fixed-under-span
• rel%closure-exists
• rel%failure_q-is-closed-under-lim
• rel%part-mapping-property
• rel_aa-is-non-expansive
• rel_fin-is-non-expansive
• relative-primality-symmetry
• relative-primality-to-primes
• relatively%prime-characterization
• relatively-prime-divisors-of-a-product
• relatively-prime-mod-characterization
• relativized-knaster-fixed-point-theorem
• removing-an-element-from-a-finite-set
• reordering-lemma
• reordering-lemma-corollary
• restricted-fixed-point-theorem
• restricted-to-range-composition-lemma
• restriction-of-datagrams
• reverse-act-associativity
• reverse-associative-law-for-multiplication-for-monoids
• reverse-filter-obligation-1
• reverse-filter-obligation-2
• reverse-left%trans-associativity
• reverse-mul-associativity
• reverse-pairs
• reverse-right%trans-associativity
• reverse-set%conjugate-associativity
• reverse-ultrametric-inequality
• reverse-ultrametric-lemma
• reverse-zero-before->
• reverse-zero-before->=
• reverse-zero-before-<
• reverse-zero-before-<=
• reverse-zero-before-=
• right%coset%app-is-total
• right%cosets-is-total
• right%cosets-membership
• right%trans->left%trans-obligation
• right%trans-associativity
• right%trans-is-total
• right%trans-left%trans-associativity
• right%trans-set%mul-associativity
• right-act-inv
• right-cancellation-law
• right-cancellation-law-for-monoids
• right-coset-inversion
• right-coset-left-identity
• right-coset-left-inverse
• right-coset-multiplication
• right-coset-right-identity
• right-coset-right-inverse
• right-cosets-are-equinumerous
• right-denominator-removal-for-equalities
• right-denominator-removal-for-inequalities
• right-denominator-removal-for-strict-inequalities
• right-group-equation
• right-inv-cancellation
• right-inverse-property
• right-iota-expression-equation-elimination
• right-left%trans-inv
• right-mul-id
• right-mul-inv
• right-mul-macete
• right-multiplicative-identity-for-monoids
• right-right%trans-inv
• right-translation-macete
• right-trivial-cancellation-law-left
• right-trivial-cancellation-law-right
• rlim-homogeneity
• run-next
• run-run
• run-run-lemma
• s(m)
• s_iface_relation-axiom
• s_init
• sandwich
• sandwich
• sandwich-lemma
• sb->gt2-obl-1
• sb->gt2-obl-2
• sb->gt2-obl-3
• sb->gt2-obl-4
• sb->gt2-obl-5
• sb->gt2-obl-6
• sb-symmetry-obl
• sb-theorem-lemma-1
• sb-theorem-lemma-2
• scalar-multiplication-by-one
• scalar-multiplication-by-zero
• schroeder-bernstein-for-types
• schroeder-bernstein-nonempty-case
• schroeder-bernstein-theorem
• schroeder-bernstein-theorem
• second-defined-entails-pair
• second-of-a-pair-is-defined
• second-projection
• second-root-of-zero
• segments-are-collinear
• self-divisibility
• sep%deg-upper-bound
• sep%dist-is-a-metric
• sep%dist-non-negative
• sep%dist-reflexive
• sep%dist-symmetric
• sep%dist-ultrametric
• sequence-bird-induction
• sequence-cases
• sequence-cases-on-right
• sequence-decomposition-on-right
• sequence-defined-monotonically
• sequence-defined-up-to-length
• sequence-induction
• sequence-induction-on-right
• sequence-not-defined-at-length
• sequences-same-length-same-domain
• set%conjugate-associativity
• set%conjugate-is-total
• set%mul-associativity
• set%mul-is-total
• set%mul-right%trans-associativity
• set-embedding-in-finite-cardinal-has-f-card
• sexp%length-of-list
• sexp%seq-is-fseq-or-total
• sexp%to%seq-0-characterization-lemma
• sexp%to%seq-drop-characterization-lemma
• silly-conditional-simplification
• singleton-e-is-a-subgroup
• singleton-equality-conversion
• singleton-equals-its-coll%closure
• singleton-has-f-card-one
• singleton-has-f-card-one-lemma-1
• singleton-has-f-card-one-lemma-2
• singleton-has-f-card-one-rewrite
• singleton-is-coll%closed
• singletons-are-collinear
• singletons-have-a-unique-member
• sm-induction
• sm-induction-biconditional
• sm-induction-biconditional-conv
• small%tails%of%summable%nonnegative%sequence
• small-distance-characterization
• small-distance-characterization-lemma
• smallest%proper%factor-defined
• smallest%proper%factor-is-prime
• smtp-filter-correctness-1
• smtp-filter-correctness-2
• smtp-filter-correctness-3
• span-definedness
• span-includes-set
• span-invariance
• splicing-continuous-functions
• splicing-continuous-functions-lemma-1
• splicing-continuous-functions-lemma-2
• splicing-pointwise-continuous-functions
• sqrt-is-an-nth%root-special-case
• sqrt-is-an-nth%root-special-case
• square-is-continuous
• stabilizer%right%cosets-are-equinumerous
• stabilizer%right%cosets-have-equal-f-card
• stabilizer%right%cosets-is-a-partition
• stabilizer-is-total
• stabilizers-are-subgroups
• state%histories-extensible
• state%histories-extensible-1
• state%histories-extensible-rev
• state%history-subsequence
• state-transition
• states-exist
• step-functions-approximate
• stop-is-a-failure
• stop-is-in-ff
• strict-monotonicity-for-multiplication
• strict-monotonicity-of-exponentiation
• strict-monotonicity-of-inverse
• strict-monotonicity-of-nth%root
• strict-negativity-for-products
• strict-positivity-for-products
• strict-positivity-for-products-of-negatives
• strict-positivity-for-products-pre-reals
• strong-cauchy-characterization-for-sep%dist
• strong-locality-of-flow%ext
• strong-locality-of-flow%ext-corollary
• strong-monotonicity-of-iterate
• strong-monotonicity-of-omega%embedding
• strong-monotonicity-of-omega%embedding-lemma
• sub-is-diff
• sub-lemma-for-processor
• sub-replacement
• subgroup->subgroup-obligation
• subgroup-is-left%trans-stabilizer
• subgroup-is-right%trans-stabilizer
• subgroups-are-groups
• subgroups-are-nonempty
• subgroups-are-subsets-of-gg%subgroup
• subgroups-closed-under-inv
• subgroups-closed-under-mul
• subgroups-contain-e
• subnet-disjointness
• subnet-is-total
• subset-embeds-in-superset
• subset-equal-if-equal-cardinality
• subset-of-finite-cardinal-has-f-card
• subset-of-finite-cardinal-is-equinumerous
• subset-of-finite-indic-is-finite
• subset-of-interval-characterization
• subset-of-nn-finite-iff-bounded
• subseteq-antisymmetry
• subseteq-reflexivity
• subseteq-transitivity
• subsets-of-finite-cardinality
• subtraction-of-fractions-lemma
• subtraction-preserves-divisibility
• subtraction-replacement
• successors%after-complement
• sum-definedness
• sum-inequality-macete
• sum-lte-product
• sum-nonnegativity
• sum-nonnegativity
• sum-of-continuous-is-continuous
• sum-of-exponents-first-corollary
• sum-of-exponents-law
• sum-of-exponents-law-lemma-0
• sum-of-exponents-law-lemma-1
• sum-of-exponents-law-pre-reals
• sum-of-exponents-second-corollary
• sum-of-fractions-lemma
• sum_kk-definedness
• sup-minus-epsilon
• sup-minus-epsilon-corollary
• sup-property-of-continuity
• sup-property-of-continuity
• sup-sum
• surjective-inverse
• surjective-inverse-with-subsort
• surjective-on-lemma
• switching
• switching
• switching-all-cases
• switching-all-cases
• sylvester
• sylvester-lemma-1
• sylvester-lemma-2
• sylvester-lemma-3
• sylvester-lemma-4
• symmetry-of-betweeness
• symmetry-of-betweeness
• symmetry-of-distance
• symmetry-of-gcd
• symmetry-of-rr-distance
• symmetry-of-sep%deg
• t%nec-t%false-rewrite
• t%nec-t%true-rewrite
• t%next-t%false-rewrite
• t%next-t%true-rewrite
• t%pos-t%false-rewrite
• t%pos-t%true-rewrite
• t%prec-p-t%true-rewrite
• t%prec-t%false-p-rewrite
• t%prec-t%true-p-rewrite
• t%unless-p-t%true-rewrite
• t%unless-t%false-p-rewrite
• t%unless-t%true-p-rewrite
• take-all
• takefirst-is-fseq
• takefirst-of-append
• takefirst-of-append-at-length
• takefirst-of-cons
• tcp_connection-embedding-lemma
• telescoping-prod-formula
• testing-characterization-of-<_may%refuse
• testing-characterization-of-<_must%refuse
• thm1
• thm2a
• thm2b
• thm3
• times-left-cancellation
• times-right-cancellation
• total-uniformly-continuous-is-continuous
• totality-of-degree
• totality-of-germ
• totality-of-multiplication;;
• totality-of-order
• tr+accessible%from
• tr-implies-accessible%from
• tr-means-next
• tr-preserves-accessible
• trace%on%line-undefined-case
• trajectories-exist
• trans-closure-of-reflexive-relation-is-reflexive
• trans-closure-of-symmetric-relation-is-symmetric
• trans-closure-of-union-of-equiv-rels-is-an-equiv-rel
• transition-maps-into-ff-condition
• transitive-closure-is-transitive
• transitivity
• transitivity-of-<=
• transitivity-of-<=-pre-reals
• transitivity-pre-reals
• translation-invariance
• triangle-inequality
• triangle-inequality-alternate-form
• triangle-inequality-for-distance
• triangle-inequality-for-rr-distance
• trichotomy
• trichotomy-pre-reals
• triple-switching
• triple-switching
• trivial-conjugation
• trivial-interval
• trivial-left-translation
• trivial-right-translation
• true%val-is-not-false
• true%val-is-true
• two-points-determine-a-line
• udp
• ultrametic-spaces-are-metric
• ultrametric-distance-bound-lemma
• ultrametric-inequality-for-distance
• ultrametric-symmetry-of-distance
• unary-eta-reduction
• unary-int-function-lemma
• unbounded-heredity
• undefined-for-negative
• undefinedness-case-of-sep%deg
• unfold-defined-expression%*_ma
• unfold-defined-expression%+_ma
• unfold-defined-expression%sub_ma
• unfolded-completeness-from-below-condition
• uniform-cauchy-implies-ptwise-cauchy
• uniform-continuity-is-closed-under-uniform-limits
• uniformly%continuous%bfun%complete
• union%of%iterates-closed-under-span
• union%of%iterates-includes-s
• union%of%iterates-is-rel%closure
• union-commutativity
• union-disjointness-left
• union-disjointness-right
• union-disjunction-conversion
• union-of-a-difference
• union-of-reflexive-relations-is-reflexive
• union-of-symmetric-relations-is-symmetric
• union-special-case
• union-with-empty
• unique-factorization-lemma-1
• unique-factorization-lemma-2
• unique-factorization-lemma-3
• unique-factorization-lemma-4
• unique-factorization-lemma-5
• unique-factorization-theorem
• uniqueness-for-pairs
• uniqueness-of-exponentiation
• uniqueness-of-exponentiation-corollary
• universe-equals-its-coll%closure
• universe-is-coll%closed
• unrefused-actions-have-next
• unrefused-actions-have-transitions
• upper-bound-of-finite-sequences
• upper-bound-of-finite-sequences-of-nn
• urg
• user%eq-abstr
• user%eq-transitivity
• value-of-a-defined-indicator-application
• value-of-monoid%prod%unordered
• vector-plus-associativity
• vector-plus-commutativity
• vector-plus-totality
• vector-times-associativity
• vector-times-associativity-left
• vector-times-left-distributivity
• vector-times-right-distributivity
• vector-times-totality
• vector-zero-identity
• weak-intermediate-value-thm
• weak-lipschitz-constant-positive
• weak-monotonicity-of-omega%embedding
• weak-monotonicity-of-omega%embedding-lemma
• weak-pasch
• weak-pasch-ordered
• weak-pasch-ordered-lemma
• weak-pasch-other
• weak-positivity-for-r^n
• well-ordering-for-integers
• well-ordering-for-natural-numbers
• zero-exponent
• zero-exponent-corollary
• zero-self-distance
• zz-*-closed
• zz-+-closed
• zz-+-closed
• zz-minus-closed
• zz-minus-closed
• zz-quotient-field
• zz-quotient-field-pre-reals
• zz-sub-closed

• Defined Constants

• >
• >=
• >=_ma
• >_ma
• <=
• <=_ma
• <_ma
• <_may%refuse
• <_must%refuse
• *_ma
• *_mod
• +_ma
• +_mod
• -_ma
• -_mod
• /_kk
• =_ma
• =_may%refuse
• ^_kk
• a%copy
• a%cosets
• a%even
• a%inf
• a%odd
• abs
• abs_ma
• abstr
• abstr_p
• accepted%actions
• accepted%transitions
• accessible
• accessible
• act_ff
• action%history
• after
• after_ff
• all%ports
• all%protocols
• alt%failure_q
• append%to%netstate
• append%to%state
• atomic%octet
• ball
• bfun%dist
• biiterate
• bound%mem
• bound%place
• bounded%non%decreasing%seq
• bounded%non%increasing%seq
• br%equiv%relation
• br%reflexive
• br%symmetric
• br%trans%closure
• br%transitive
• br%union
• c%copy
• c%copy%fn
• c%fill
• c%redirect
• c%redirect%fn
• cauchy
• check%fr%condition
• class%a
• class%b
• class%c
• class%d
• class%e
• closure
• coll
• coll
• coll%closed
• coll%closure
• coll_set
• coll_set
• comb
• combinations
• compact
• complete
• compose%filter%modules
• congruent
• conjugate%class
• connected
• connecting%lines
• connecting%lines%through
• continuous
• continuous%at%point
• continuous%at%point%rr
• contraction
• convergent%to%infinity
• copy
• copy%fn
• degree
• delta
• delta%step%approximant
• delta%width
• deny%all%inbound%rule
• deny%all%module
• deny%all%outbound%rule
• deriv
• diffuse
• directly%connected
• discrete%lim
• discrete%set
• div
• div_ma
• divides
• dseq
• dudek
• e%subgroup
• empty%state
• entry%index
• equiv%class
• equiv%class_q
• equiv%on%classes%unary
• equiv%predicate
• eqv%may%refuse
• even
• every%tcp%connection%is%generic
• extendable
• f_indic_act
• factorial
• failure_q
• failures
• false%val
• fct%mapping
• ff%dist
• filter
• first%entry
• floor
• flow%ext
• fn%approx
• from%region
• g%h%ok
• g%h%ok_2
• gcd
• generator
• generic%tcp%connection
• generic%tcp%filter%module
• generic%tcp%rule%1
• generic%tcp%rule%2
• germ
• gg%subgroup
• h
• h%ok
• has%profile
• history
• history
• hosts%of%spnet
• ideal
• iface%in%to%out
• iface%out%to%in
• iface_a
• iface_b
• ifaces%of%host
• ifaces%of%spnet
• ifill
• ii%locally%lipschitz%bound
• in%language
• independent%rules
• init%eqv
• initiates%tcp%connection
• integrable
• integral
• is%false
• is%loopback%spnet
• is%multi%homed
• is%point%to%point%spnet
• is%single%homed
• is%true
• isolated
• istore
• istore%simple
• last%a%index
• le
• left%trans
• lim
• lim%rr
• limited%externally%initiated%tcp%connections
• limited%smtp%connections
• line
• lipschitz%bound
• lipschitz%bound%on
• loop
• loopback%iface
• lower
• lub_rr
• make%default
• make%gamma
• make%istate_p
• make%one%rule%filter%module
• make%three%rule%filter%module
• make%two%rule%filter%module
• make%zero%rule%filter%module
• map
• max
• max%on%set
• maximal
• maximum
• may%accept%after
• may%refuse%after
• min
• minus
• mod
• mod_ma
• monoid%prod%unordered
• monotone
• monotone%between
• mu
• must%accept%after
• must%refuse%after
• neg_1
• net%id
• network%is%conventional
• next
• next%hop%iface
• no%externally%initiated%tcp%connections
• no%factors%between
• no%smtp%connections
• no%spoofing%module
• no%spoofing%policy
• no%spoofing%rule
• normal
• normalizer
• nth
• nth%cdr
• nth%root
• null%state%condition
• nullify%on%set
• octet%le
• octet%lt
• octet%to%nn
• odd
• omega
• on%connecting%line
• on%connecting%line%through
• only%smtp%connections
• open
• open%ball
• opposite%direction
• orbit
• p%list_q
• parallel
• positive%prime
• posrat%exp
• power
• prec%increasing
• prec%lim%inf
• prec%majorizes
• prec%sup
• preceding
• pred%to%rel
• prefix
• prime%decomposition
• primitive
• princ%ideal
• promote
• quotient
• raise
• rangenet
• refused%actions
• refused%transitions
• regular%place
• rel%closed
• rel%closure
• rel%failure_q
• rel%part
• rel_aa
• relatively%prime
• rev%prec
• right%coset%app
• right%cosets
• right%trans
• rlim
• routing%fn
• seg
• sep%deg
• sep%dist
• set%conjugate
• set%conjugate%class
• set%min
• set%mul
• set%normalizer
• set%prec
• sexp%length
• sexp%to%seq
• smallest%factor
• smtp%connection
• smtp%filter%condition%1
• smtp%filter%condition%2
• smtp%filter%condition%3
• smtp%filter%condition%4
• smtp%filter%specification
• snapshot%not%visible
• span
• spnet%is%conventional
• spnets%of%host
• sqrt
• stabilizer
• stabilizer%right%cosets
• state%embedding
• state%history
• state%history
• step%fn
• stop_ff
• sub
• sub_kk
• sub_ma
• sub_vv
• subgroup
• subnet
• subspace%closed
• subspace%dense
• successors%after
• summable%nonnegative
• support
• t%and
• t%false
• t%nec
• t%next
• t%not
• t%or
• t%pos
• t%prec
• t%true
• t%unless
• tcp%connection
• trace%on%line
• trajectory
• trans%in%out
• trans%out%in
• transition
• true%val
• twist
• ub_rr
• uniformly%continuous
• union%of%iterates
• unrefused
• user%eq
• uses%service
• vertex%incidence%set
• weakly%lipschitz%between
• zz%interval
• zz%quotient

• Recursively Defined Constants

• ^
• a%seq
• accessible%from
• br%partial%trans%closure
• comb_kk
• connected
• gcd_ma
• gcd_rho
• iterate
• list
• monoid%prod
• multiple
• nn%quotient
• omega%embedding
• opseq%state
• prod
• prod_kk
• run
• sum
• sum_kk

• Compound Macetes

• monoid-cancellation-laws
• comb_kk-values
• compute-card
• covers-direct-image-to-inverse-image-conversion-macete
• indicator-conversions
• iota-abstraction-macete
• eliminate-iota-macete
• eliminate-forsome-macete
• direct-image-to-inverse-image-conversion-macete
• indicator-facts-macete
• rewrite-rules-for-pairs
• drop-cons-and-simplify
• in_seq-macete
• sequence-length
• le-contains-point
• simplify-set-translations
• simplify-actions
• group-cancellation-laws
• lct-macete
• simplify-normal-subgroup-expressions
• simplify-right-coset-expressions
• subgroup-membership
• abstraction
• composite-continuity-macete
• real-fn-abstraction
• polynomial-continuity-macete
• simplify-subnet-disjointness-assertion
• ns-fractional-expression-manipulation
• fractional-expression-manipulation
• integer-induction
• definedness-manipulations
• factorial-reduction
• abstraction-for-sequences
• solve-product-equation-or-inequality
• crude-primality-test

• Defined Atomic Sorts

• a%cosets%sort
• action
• b%sort
• bb
• bfun
• boole
• continuous%bfun
• expr%seq
• ff
• ff_aa
• ff_p
• filtered%states
• iface%seq
• ifaces
• ii
• int
• jj
• lines
• netstates
• nn
• ports
• sexp%list
• state%seq
• states
• total%fns
• traject
• unif%continuous%bfun
• uu_q
• zz_mod

• Quasi-Constructors

• append
• collapse
• cons
• constrict
• countable%cover
• drop
• embeds
• equinumerous
• f-seq?
• finite%cover
• finite-cardinality
• finite-indicator?
• finite-sort?
• first
• group
• i-big-intersection
• i-big-union
• i-complement
• i-cross-product
• i-difference
• i-disjoint
• i-empty-indicator
• i-empty-indicator?
• i-in
• i-intersection
• i-nonempty-indicator?
• i-partition?
• i-singleton
• i-subset
• i-subseteq
• i-sym-difference
• i-union
• in_seq
• invariant
• length
• m-bijective-on?
• m-bijective?
• m-composition
• m-domain
• m-id
• m-image
• m-injective-on?
• m-injective?
• m-inverse
• m-inverse-image
• m-range
• m-restrict
• m-restrict2
• m-surjective-on?
• m-surjective?
• nil
• pair
• pair?
• predicate-to-indicator
• second
• sort-to-indicator
• takefirst