IMPS: An Interactive Mathematical Proof System

Copyright (c) 1990-2000 The MITRE Corporation

Authors: W. M. Farmer, J. D. Guttman, F. J. Thayer

IMPS Theory Library


Contents

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
  • functions-on-a-graded-set
  • 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
  • graded-monoid
  • graded-monoid-transition-system
  • 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
  • parametrized-graded-monoid
  • 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
  • relativized-graded-monoid
  • 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-additive-rr
  • 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
  • degree-equivalence-to-functions-on-a-graded-set
  • degree-equivalence-to-functions-on-a-graded-set
  • degree-equivalence-to-graded-monoid
  • external-smtp
  • fields-to-rr
  • fields-to-rr-extended
  • finite-specialization-of-rgm
  • functions-on-a-graded-set-to-graded-monoid
  • 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-additive-group
  • group-to-field-multiplicative-group
  • groups->subgroup
  • groups-to-additive-kk
  • groups-to-additive-rr
  • 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-into-a-pointed-metric-space-to-parametrized-graded-monoid
  • mappings-on-interval-into-ns-to-rr
  • mappings-pointed-metric-spaces-2-tuples
  • monoid-transition-system-to-directed-monoid-theory
  • monoids-to-additive-kk
  • monoids-to-groups
  • ms-subspace-to-graded-monoid
  • 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
  • pointed-metric-space-to-graded-monoid
  • 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
  • add-left-cancellation
  • add-neg_1-0
  • add-neg_1-typical-case
  • add-one-special-case
  • add-one-typical-case
  • add-right-cancellation
  • addition-congruence-invariance-lemma
  • addition-of-fractions-left
  • addition-of-fractions-right
  • addition-of-one-destroys-divisibility
  • addition-preserves-divisibility
  • additive-identity-for-fields
  • additive-inverse-for-fields
  • additivity-of-deriv
  • additivity-of-integral
  • additivity-of-real-limit
  • additivity-of-real-limit-corollary
  • additivity-of-rr-derivative
  • addr_a-is-an-address-of-an-interface
  • addr_b-is-an-address-of-an-interface
  • address%and-is-total
  • address%lt-transitivity
  • address%xor-is-total
  • aix
  • all-addresses-subnet-macete
  • all-class-a-addresses-subnet-macete
  • all-class-b-addresses-subnet-macete
  • all-class-c-addresses-subnet-macete
  • 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-addition
  • associative-law-for-addition-for-fields
  • associative-law-for-addition-pre-reals
  • 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
  • ball-subset-larger-radius-open-ball
  • 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-additivity-case-1
  • biiterate-additivity-case-2
  • biiterate-additivity-case-3
  • biiterate-additivity-case-4
  • 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
  • bounded-rad-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-c%shadow-c%copy-defined
  • c%redirect-c%shadow-c%copy-definedness-case3
  • c%redirect-no-op
  • c%shadow-c%copy-definedness
  • c%shadow-default
  • c%shadow-definedness
  • c%shadow-no-op
  • c%shadow-of-c%copy-definedness
  • 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-addition
  • commutative-law-for-addition-for-fields
  • commutative-law-for-addition-pre-reals
  • 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-additivity-of-integral
  • 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-addresses-lemma
  • 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
  • factor-quadratic-polynomial
  • 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-added-to-refusal-sets
  • 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
  • gamma-c%shadow-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
  • graded-monoid-fn%approx-existence
  • graded-monoid-fn%approx-monotonicity
  • graded-monoid-fn%approx-reflexivity
  • graded-monoid-fn%approx-separation
  • graded-monoid-fn%approx-symmetry
  • graded-monoid-fn%approx-transitivity
  • graded-monoid-fn%dist-non-negative
  • graded-monoid-fn%dist-reflexive
  • graded-monoid-fn%dist-symmetric
  • graded-monoid-fn%dist-triangle-inequality
  • group-commutativity
  • group-to-field-additive-group-obl-1
  • group-to-field-additive-group-obl-2
  • 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-additivity
  • iterate-additivity
  • 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
  • load-section
  • 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-interface-has-loopback%address
  • loopback-interface-has-loopback%mask
  • 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-additivity-lemma
  • multiple-commutes-with-negation
  • multiple-commutes-with-negation-corollary
  • multiple-commutes-with-negation-in-group
  • multiple-difference-lemma
  • multiple-is-additive
  • multiple-is-additive-in-group
  • multiple-is-homogenuous
  • multiple-of-group-identity
  • multiple-totality
  • multiple-totality-with-range
  • multiplication-by-a-constant-is-continuous
  • multiplication-by-a-constant-is-quadratic
  • 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_addr-is-an-address-of-out_iface-spnet
  • next_hop_iface-lemma
  • nil-is-fseq
  • nn-addition-rewrite
  • 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-additive-property
  • 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
  • preferred-c%shadow-c%copy-definedness
  • 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
  • quadratic-is-continuous
  • quadratic-is-uniformly-continuous
  • 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-additivity
  • rlim-homogeneity
  • run-next
  • run-run
  • run-run-lemma
  • s(m)
  • s_address_relation-axiom
  • s_iface_relation-axiom
  • s_init
  • s_mask_relation-axiom
  • 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
  • single-address-to-subnet-specification
  • 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
  • source%address(d)
  • source%address(d)
  • 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
  • square-is-quadratic
  • 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-interval-additivity
  • 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-addition
  • 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
  • vs-addition-of-fractions-left
  • vs-addition-of-fractions-right
  • 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
  • addr%to%iface
  • address%and
  • address%le
  • address%lt
  • address%xor
  • addresses%of%host
  • addresses%of%spnet
  • adjacent%edges
  • adjacent%vertices
  • after
  • after_ff
  • all%addresses
  • all%class%a%addresses
  • all%class%b%addresses
  • all%class%c%addresses
  • 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
  • c%shadow
  • cauchy
  • check%fr%condition
  • class%a
  • class%a%mask
  • class%b
  • class%b%mask
  • class%c
  • class%c%mask
  • 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%address
  • loopback%iface
  • loopback%mask
  • 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
  • masked%off
  • masked%on
  • masks%of%host
  • masks%of%spnet
  • 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
  • quadratic%bound
  • quadratic%bound%at%point
  • quotient
  • rad%dist
  • 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
  • shadow%set
  • 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%address
  • spnet%is%conventional
  • spnet%mask
  • 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
  • simplify-address-set-disjointness-assertion
  • simplify-address-expression
  • ns-fractional-expression-manipulation
  • fractional-expression-manipulation
  • integer-induction
  • definedness-manipulations
  • factorial-reduction
  • abstraction-for-sequences
  • solve-product-equation-or-inequality
  • solve-quadratic-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
  • masks
  • 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