#ABCMIZ_0
G3 K0 L0 M1 O7 R2 U4 V7 
VMizar-widening-like
GAdjectiveStr
Uadjectives
Unon-op
Madjective
Onon-
Vwithout_fixpoints
GTA-structure
Uadj-map
Oadjs
Vconsistent
Vadj-structured
Otypes
Vadjs-typed
Ris_applicable_to
Oast
Osub
GTAS-structure
Usub-map
Vnon-absorbing
Vsubjected
Ris_properly_applicable_to
O@-->
Oradix
#ABCMIZ_1
G0 K0 L0 M9 O26 R0 U0 V10 
Ovarcl
Mvariable
Ovars
OQuasiLoci
Mquasi-loci
Oa_Type
Oan_Adj
Oa_Term
Onon_op
Vconstructor
OMinConstrSign
MConstructorSignature
Vinitialized
OModes
OAttrs
OConstructors
Okind_of
Oloci_of
Oindex_of
OMaxConstrSign
OMSVars
Vground
Vcompound
Mexpression
OQuasiTerms
Mquasi-term
O-trm
ONon
OQuasiAdjs
Mquasi-adjective
Vpure
OQuasiTypes
Mquasi-type
Othe_base_of
OVarPoset
Ovars-function
Vwith_an_operation_for_each_sort
Vwith_missing_variables
Mterm-transformation
Vsubstitution
Mvaluation
Virrelevant
Vrelevant
Oidval
Oat 128
#ABCMIZ_A
G0 K0 L0 M2 O7 R7 U0 V2 
Vstandardized
Rmatches_with
Runifies
Rare_unifiable
Rare_weakly-unifiable
Ris_a_unification_of
Ris_a_general-unification_of
Ris_a_general-unifier_of
Msubexpression
Othe_constr_of
Oconstrs
Omain-constr
Oargs
Obase_exp_of
Mtype-distribution
Oset-constr
Oset-type
Varity-rich
#ABIAN
G0 K0 L0 M0 O1 R3 U0 V3 
Veven
Vodd
Ris_a_fixpoint_of
Rhas_a_fixpoint
Rhas_no_fixpoint
Vcovering
O=_
#ABSVALUE
G0 K0 L0 M0 O1 R0 U0 V0 
Osgn
#AFF_1
G0 K0 L0 M0 O0 R0 U0 V1 
Vbeing_line
#AFF_2
G0 K0 L0 M0 O0 R0 U0 V14 
Vsatisfying_PPAP
VPappian
Vsatisfying_PAP_1
VDesarguesian
Vsatisfying_DES_1
Vsatisfying_DES_2
VMoufangian
Vsatisfying_TDES_1
Vsatisfying_TDES_2
Vsatisfying_TDES_3
Vtranslational
Vsatisfying_des_1
Vsatisfying_pap
Vsatisfying_pap_1
#AFF_3
G0 K0 L0 M0 O0 R0 U0 V8 
Vsatisfying_DES1
Vsatisfying_DES1_1
Vsatisfying_DES1_2
Vsatisfying_DES1_3
Vsatisfying_DES2
Vsatisfying_DES2_1
Vsatisfying_DES2_2
Vsatisfying_DES2_3
#AFF_4
G0 K0 L0 M0 O0 R1 U0 V1 
Vbeing_plane
Ris_coplanar
#AFINSQ_1
G0 K1 L1 M1 O3 R0 U0 V0 
MXFinSequence
K<%
L%>
O<%> 254
O^omega
OReplace
#AFINSQ_2
G0 K0 L0 M0 O2 R2 U0 V0 
OSgm0
R<N<
R<N=
OSubXFinS
#AFPROJ
G0 K0 L0 M0 O10 R0 U0 V0 
OAfLines
OAfPlanes
OLinesParallelity
OPlanesParallelity
OLDir
OPDir
ODir_of_Lines
ODir_of_Planes
OInc_of_Dir
OProjHorizon
#AFVECT0
G0 K0 L0 M2 O4 R3 U0 V1 
VWeakAffVect-like
MWeakAffVect
RMDist
OPSym
OPadd
OPcom
OGroupVect
MProper_Uniquely_Two_Divisible_Group
Ris_Iso_of
Rare_Iso
#AFVECT01
G0 K0 L0 M1 O0 R0 U0 V1 
VWeakAffSegm-like
MWeakAffSegm
#ALGSEQ_1
G0 K0 L0 M1 O0 R1 U0 V1 
Vfinite-Support
MAlgSequence
Ris_at_least_length_of
#ALGSPEC1
G0 K0 L0 M2 O1 R1 U0 V0 
O-indexing
Mrng-retract
Rform_a_replacement_in
MExtension
#ALGSTR_0
G6 K0 L0 M0 O6 R0 U2 V18 
GaddMagma
UaddF
OTrivial-addMagma
Vleft_add-cancelable
Vright_add-cancelable
Vadd-cancelable
GaddLoopStr
OTrivial-addLoopStr
Vleft_complementable
Vright_complementable
Vcomplementable
GmultMagma
UmultF
OTrivial-multMagma
Vleft_mult-cancelable
Vright_mult-cancelable
Vmult-cancelable
GmultLoopStr
OTrivial-multLoopStr
Vleft_invertible
Vright_invertible
Vinvertible
GmultLoopStr_0
OTrivial-multLoopStr_0
Valmost_left_cancelable
Valmost_right_cancelable
Valmost_cancelable
Valmost_left_invertible
Valmost_right_invertible
Valmost_invertible
GdoubleLoopStr
OTrivial-doubleLoopStr
#ALGSTR_1
G0 K0 L0 M5 O2 R0 U0 V6 
OExtract
Vleft_zeroed
Vadd-left-invertible
Vadd-right-invertible
VLoop-like
MLoop
Vcancelable
MmultLoop
MmultGroup
OmultEX_0
VmultLoop_0-like
MmultLoop_0
MmultGroup_0
#ALGSTR_2
G0 K0 L0 M6 O0 R0 U0 V0 
MdoubleLoop
MleftQuasi-Field
MrightQuasi-Field
MdoublesidedQuasi-Field
M_Skew-Field
M_Field
#ALGSTR_3
G1 K0 L0 M1 O4 R0 U1 V1 
GTernaryFieldStr
UTernOp
OTern
Oternaryreal
OTernaryFieldEx
Otern
VTernary-Field-like
MTernary-Field
#ALGSTR_4
G0 K0 L0 M2 O13 R1 U0 V0 
OIFXFinSequence
Rextends
OClassOp
MRelators
Oequ_rel
Oequ_kernel
MmultSubmagma
Othe_mult_induced_by
Othe_submagma_generated_by
Ofree_magma_seq
Ofree_magma
Ofree_magma_carrier
Ofree_magma_mult
Olength
Ocanon_image
Ofree_magmaF
#ALG_1
G0 K0 L0 M1 O7 R1 U0 V0 
OExtendRel
MCongruence
Ris_representatives_FS
OQuotOp
OQuotOpSeq
OQuotUnivAlg
ONat_Hom
OCng
OHomQuot
#ALI2
G0 K0 L0 M1 O0 R0 U0 V0 
Mcontraction
#ALTCAT_1
G2 K2 L2 M4 O4 R0 U1 V9 
GAltGraph
UArrows
Mobject
K<^
L^>
K{|
L|}
MBinComp
Vwith_right_units
Vwith_left_units
GAltCatStr
Vcompositional
OFuncComp
Vquasi-functional
Vsemi-functional
Vpseudo-functional
OEnsCat
Vwith_units
Mcategory
Oidm
Vquasi-discrete
Vpseudo-discrete
Mdiscrete_category
ODiscrCat
#ALTCAT_2
G0 K0 L0 M2 O5 R1 U0 V1 
Rcc=
Othe_hom_sets_of
Othe_comps_of
OAlter
Othe_empty_category
MSubCatStr
OObCat
Vid-inheriting
Msubcategory
#ALTCAT_3
G0 K0 L0 M0 O0 R3 U0 V3 
Ris_left_inverse_of
Ris_right_inverse_of
Viso
Rare_iso
Vmono
V_zero
#ALTCAT_4
G0 K0 L0 M0 O5 R0 U0 V0 
OAllMono
OAllEpi
OAllRetr
OAllCoretr
OAllIso
#AMISTD_1
G0 K0 L0 M2 O8 R0 U0 V6 
MIL-Subset
Vjump-only
ONIC
OJUMP
OSUCC
VInsLoc-antisymmetric
OSTC
Oil.
Olocnum
ONextLoc
Vreally-closed
Vpara-closed
OLastLoc
Vhalt-ending
Vunique-halt
Mpre-Macro
#AMISTD_2
G0 K0 L0 M0 O5 R0 U0 V5 
OAddressParts
Vwith_explicit_jumps
Vwithout_implicit_jumps
Vins-loc-free
OStop
OIncAddr
VIC-good
VExec-preserving
OCutLastLoc
ORelocated
#AMISTD_3
G0 K0 L0 M0 O5 R0 U0 V0 
OTrivialInfiniteTree
OFirstLoc
OLocNums
OLocSeq
OExecTree
#AMI_1
G1 K0 L0 M10 O14 R4 U4 V11 
GAMI-Struct
UInstruction-Counter
UInstructions
UObject-Kind
UExecution
OTrivial-AMI
Vstored-program
MInstruction-Location
MInstruction
OIC
OObjectKind
OExec
Ohalt
VIC-Ins-separated
Vsteady-programmed
Vdefinite
OCurInstr
MPartState
MFinPartState
OProgramPart
Rhalts_on
Vrealistic
OFinPartSt
OData-Locations
Vautonomic
Vprogrammable
Mpre-program
Rdoes_not_compute
Vcomputable
MProgram
OInsCode
OAddressPart
Vstandard-ins
OInsCodes
MInsType
MIL-FinSequence
MIL-Function
MIL-DecoratedTree
OStart-At
Rstarts_at
Rhalts_at
ODataPart
Vdata-only
Vhalt-free
#AMI_2
G0 K0 L0 M1 O13 R0 U0 V0 
OSCM-Halt
OSCM-Data-Loc
OSCM-Memory
OSCM-Instr
OSCM-OK
MSCM-State
OSCM-Chg
Oaddress_1
Oaddress_2
Ojump_address
Ocjump_address
Ocond_address
OSCM-Exec-Res
OSCM-Exec
#AMI_3
G0 K0 L0 M1 O9 R0 U0 V0 
OSCM
MData-Location
OAddTo
OSubFrom
OMultBy
ODivide
Ogoto
O=0_goto
O>0_goto
Odl.
#AMI_4
G0 K0 L0 M0 O2 R0 U0 V0 
OEuclide-Algorithm
OEuclide-Function
#AMI_7
G0 K0 L0 M0 O2 R0 U0 V2 
Vwith_non_trivial_Instructions
Vwith_non_trivial_ObjectKinds
OOut_\_Inp
OOut_U_Inp
#ANALMETR
G1 K0 L0 M2 O3 R2 U1 V2 
RGen
Rare_Ort_wrt
OOrthogonality
GParOrtStr
Uorthogonality
OAMSpace
OAf
VOrtAfSp-like
MOrtAfSp
VOrtAfPl-like
MOrtAfPl
#ANALOAF
G1 K0 L0 M2 O2 R1 U1 V2 
R//
GAffinStruct
UCONGR
ODirPar
OOASpace
VOAffinSpace-like
MOAffinSpace
V2-dimensional
MOAffinPlane
#ANALORT
G0 K0 L0 M0 O6 R2 U0 V0 
OOrtm
OOrte
Rare_COrte_wrt
Rare_COrtm_wrt
OCORTE
OCORTM
OCESpace
OCMSpace
#ANPROJ_1
G0 K0 L0 M0 O5 R2 U0 V0 
Rare_Prop
Rare_LinDep
OProportionality_as_EqRel_of
ODir
OProjectivePoints
OProjectiveCollinearity
OProjectiveSpace
#ANPROJ_2
G0 K0 L0 M2 O0 R5 U0 V3 
Rare_Prop_Vect
Rlie_on_a_triangle
Rare_perspective
Rlie_on_an_angle
Rare_half_mutually_not_Prop
VVebleian
Vat_least_3rank
MCollProjectiveSpace
Vat_most-3-dimensional
MCollProjectivePlane
#AOFA_000
G0 K0 L0 M4 O12 R6 U0 V8 
Rnin
Oorbit
OGenerators
Vwith_empty-instruction
Vwith_catenation
Vwith_if-instruction
Vwith_while-instruction
MpreIfWhileAlgebra
MAlgorithm
OEmptyIns
O\; 16
Oif-then-else
Oif-then
Owhile
Ofor-do
OElementaryInstructions
OECIW-signature
VECIW-strict
MIfWhileAlgebra
Vcomplying_with_empty-instruction
Vcomplying_with_catenation
Rcomplies_with_if_wrt
Rcomplies_with_while_wrt
MExecutionFunction
Riteration_terminates_for
Oiteration-degree
OTerminatingPrograms
Vabsolutely-terminating
Ris_terminating_wrt
Ris_invariant_wrt
#AOFA_I00
G0 K0 L0 M6 O13 R2 U0 V0 
Oleq 32
Ogt 32
Oeq 32
MEnumeration
MDenumeration
MINT-Variable
MINT-Expression
MINT-Array
Ris_assignment_wrt
Rform_assignment_wrt
OINT-ElemIns
MINT-Exec
O+= 32
O*= 32
Oswap
O%= 32
O/= 32
Ois_odd
Ois_even
Ogeq 32
Olt 32
#ARMSTRNG
G1 K0 L0 M4 O13 R8 U3 V19 
OMaximal_in
Ris_/\-irreducible_in
Ris_/\-reducible_in
O/\-IRR
V(B1)
V(B2)
GDB-Rel
UAttributes
UDomains
URelationship
MSubset-Relation
MDependency-set
ODependencies
MDependency
R>|>
Rholds_in
ODependency-str
Ris_at_least_as_informative_as
ODependencies-Order
V(F2)
V(DC1)
V(F1)
V(DC2)
V(F3)
V(F4)
Vfull_family
MFull-family
V(DC3)
OMaximal_wrt
R^|^
V(M1)
V(M2)
V(M3)
Osaturated-subsets
Oclosed_attribute_subset
Odeps_encl_by
Oenclosure_of
ODependency-closure
Ris_generator-set_of
Ocandidate-keys
V(C1)
Vwithout_proper_subsets
V(C2)
V(DC4)
V(DC5)
V(DC6)
Ocharact_set
Ris_p_i_w_ncv_of
#ARROW
G0 K0 L0 M0 O2 R4 U0 V0 
OLinPreorders
OLinOrders
R<=_
R>=_
R<_
R>_
#ARYTM_0
G0 K1 L1 M0 O2 R0 U0 V0 
Oopp 128
Oinv
K[*
L*]
#ARYTM_1
G0 K0 L0 M0 O2 R0 U0 V0 
O-' 32
O- 32
#ARYTM_2
G0 K0 L0 M0 O4 R0 U0 V0 
ODEDEKIND_CUTS
OREAL+
ODEDEKIND_CUT 130
OGLUED 130
#ARYTM_3
G0 K0 L0 M0 O11 R4 U0 V0 
Oone 128
Rare_relative_prime
Rdivides
Olcm 32
Ohcf 32
ORED
ORAT+
Onumerator 150
Odenominator 150
O/
Oquotient
O+ 32
O*' 128
R<='
R<
#ASYMPT_0
G0 K0 L0 M0 O4 R2 U0 V6 
Vlogbase
Veventually-nonnegative
Veventually-positive
Veventually-nonzero
Veventually-nondecreasing
Rmajorizes
OBig_Oh
OBig_Omega
OBig_Theta
Otaken_every
Ris_smooth_wrt
Vsmooth
#ASYMPT_1
G0 K0 L0 M0 O7 R0 U0 V0 
Oseq_a^
Oseq_logn
Oseq_n^
Oseq_const
Oseq_n!
OPOWEROF2SET
OStep1
#AUTALG_1
G0 K0 L0 M1 O6 R0 U0 V0 
OUAAut
OUAAutComp
OUAAutGroup
MMSFunctionSet
OMSAAut
OMSAAutComp
OMSAAutGroup
#AUTGROUP
G0 K0 L0 M0 O6 R0 U0 V0 
OAut
OAutComp
OAutGroup
OInnAut
OInnAutGroup
OConjugate
#BAGORDER
G0 K0 L0 M1 O14 R0 U0 V1 
OTotDegree
MTermOrder
OLexOrder
Vadmissible
OInvLexOrder
OGraded
OGrLexOrder
OGrInvLexOrder
OBlockOrder
ONaivelyOrderedBags
OPosetMin
OPosetMax
OFinOrd-Approx
OFinOrd
OFinPoset
OMinElement
#BCIALG_1
G2 K0 L0 M2 O4 R0 U1 V13 
GBCIStr
UInternalDiff
GBCIStr_0
Vbeing_B
Vbeing_C
Vbeing_I
Vbeing_K
Vbeing_BCI-4
Vbeing_BCK-5
OBCI-EXAMPLE 16
MBCI-algebra
MBCK-algebra
OBCK-part
OAtomSet
Vgenerated_by_atom
OBranchV
Vquasi-associative
Vpositive-implicative
Vweakly-positive-implicative
Vweakly-implicative
Vp-Semisimple
Valternative
#BCIALG_2
G0 K0 L0 M3 O6 R0 U0 V3 
Vleast
Vgreatest
Vnilpotent
ML-congruence
MR-congruence
MI-congruence
OIConSet
OConSet
OLConSet
ORConSet
OEqClaOp
OzeroEqC
#BCIALG_3
G0 K0 L0 M1 O0 R0 U0 V9 
Vbeing_greatest
Vbeing_positive
VBCI-commutative
VBCI-weakly-commutative
Vinvolutory
Vbeing_Iseki
VIseki_extension
MCommutative-Ideal
VBCK-positive-implicative
VBCK-implicative
#BCIALG_4
G1 K0 L0 M3 O5 R0 U1 V4 
GBCIStr_1
UExternalDiff
Vwith_condition_S
OBCI_S-EXAMPLE
MBCI-Algebra_with_Condition(S)
OCondition_S
OAdjoint_pGroup
OProduct_S
MBCK-Algebra_with_Condition(S)
OInitial_section
Vbeing_SB-1
Vbeing_SB-2
Vbeing_SB-4
Msemi-Brouwerian-algebra
#BCIALG_5
G0 K0 L0 M0 O1 R0 U0 V1 
Vquasi-commutative
Op-Semisimple-part
#BCIALG_6
G0 K0 L0 M1 O4 R0 U0 V2 
OBCI-power 124
Vfinite-period
MBCI-homomorphism
Visotonic
OHKOp
OzeroHK
OHK
#BCIIDEAL
G0 K0 L0 M4 O1 R0 U0 V0 
Oinitial_section
Massociative-ideal
Mp-ideal
Mimplicative-ideal
Mpositive-implicative-ideal
#BHSP_1
G1 K0 L0 M1 O0 R0 U1 V1 
GUNITSTR
Uscalar
VRealUnitarySpace-like
MRealUnitarySpace
#BHSP_3
G0 K0 L0 M0 O0 R1 U0 V2 
VCauchy
Ris_compared_to
VHilbert
#BHSP_5
G0 K0 L0 M2 O5 R0 U0 V0 
Osetop_SUM
OFunc_Seq
Osetopfunc
Osetop_xPre_PROD
Osetop_xPROD
MOrthogonalFamily
MOrthonormalFamily
#BHSP_6
G0 K0 L0 M0 O2 R1 U0 V2 
Osetsum
Vsummable_set
Vweakly_summable_set
Ris_summable_set_by
Osum_byfunc
#BILINEAR
G0 K0 L0 M2 O12 R0 U0 V6 
MForm
ONulForm
OFunctionalFAF
OFunctionalSAF
OFormFunctional
VadditiveFAF
VadditiveSAF
VhomogeneousFAF
VhomogeneousSAF
Mbilinear-Form
Oleftker
Orightker
Odiagker
OLKer
ORKer
OLQForm
ORQForm
OQForm
Vdegenerated-on-left
Vdegenerated-on-right
#BINARITH
G0 K0 L0 M0 O4 R1 U0 V0 
Ocarry
OBinary
OAbsval
Oadd_ovfl
Rare_summable
#BINARI_2
G0 K0 L0 M0 O5 R0 U0 V0 
OBin1
ONeg2
OIntval
OInt_add_ovfl
OInt_add_udfl
#BINARI_3
G0 K0 L0 M0 O1 R0 U0 V0 
O-BinarySequence
#BINARI_4
G0 K0 L0 M0 O2 R0 U0 V0 
OMajP
O2sComplement
#BINOM
G0 K0 L0 M0 O2 R0 U0 V0 
ONat-mult-left
ONat-mult-right
#BINOP_1
G0 K0 L0 M2 O1 R6 U0 V3 
MUnOp
MBinOp
Vcommutative
Vassociative
Vidempotent
Ris_a_left_unity_wrt
Ris_a_right_unity_wrt
Ris_a_unity_wrt
Othe_unity_wrt 128
Ris_left_distributive_wrt
Ris_right_distributive_wrt
Ris_distributive_wrt
#BINOP_2
G0 K0 L0 M0 O24 R0 U0 V0 
Ocompcomplex 128
Oinvcomplex
Oaddcomplex 128
Odiffcomplex 128
Omultcomplex 128
Odivcomplex
Ocompreal
Oinvreal
Oaddreal
Odiffreal 128
Omultreal
Odivreal
Ocomprat
Oinvrat
Oaddrat
Odiffrat
Omultrat
Odivrat
Ocompint
Oaddint
Odiffint
Omultint
Oaddnat
Omultnat
#BINTREE1
G0 K0 L0 M0 O1 R0 U0 V1 
Oroot-label
Vbinary
#BINTREE2
G0 K0 L0 M0 O2 R0 U0 V0 
ONumberOnLevel
OFinSeqLevel
#BIRKHOFF
G0 K0 L0 M0 O1 R0 U0 V0 
O-hash
#BOOLMARK
G0 K0 L0 M1 O2 R2 U0 V0 
OBool_marks_of
MBoolean_marking
Ris_firable_on
Ris_not_firable_on
OFiring
#BORSUK_1
G0 K0 L0 M2 O10 R2 U0 V2 
OBase-Appr
OPr1
OPr2
OTrivDecomp
Ospace
OProj 128
OTrivExt 128
Mu.s.c._decomposition
VDECOMPOSITION-like
MDECOMPOSITION
OI[01]
O0[01]
O1[01]
Vbeing_a_retraction
Ris_a_retract_of
Ris_an_SDR_of
#BORSUK_2
G0 K0 L0 M0 O0 R2 U0 V1 
Rare_connected
Varcwise_connected
Rare_homotopic
#BORSUK_4
G0 K0 L0 M0 O1 R0 U0 V0 
OI(01)
#BORSUK_5
G0 K0 L0 M0 O1 R0 U0 V0 
OIRRAT
#BORSUK_6
G0 K0 L0 M1 O10 R0 U0 V0 
ORePar
O1RP
O2RP
O3RP
OLowerLeftUnitTriangle
OIAA
OUpperUnitTriangle
OIBB
OLowerRightUnitTriangle
OICC
MHomotopy
#BROUWER
G0 K0 L0 M0 O4 R0 U0 V0 
ODiffElems
OTdisk
OHC
OBR-map
#BSPACE
G0 K0 L0 M0 O6 R0 U0 V1 
OZ_2
O\*\
Obspace-sum
Obspace-scalar-mult
Obspace
VSingleton
Osingletons
#BVFUNC_1
G0 K0 L0 M0 O7 R1 U0 V0 
O'imp' 15
O'eqv' 14
OO_el 255
OI_el 255
OB_INF 255
OB_SUP 255
Ris_dependent_of
OGPart
#BVFUNC_2
G0 K0 L0 M0 O3 R3 U0 V2 
Ris_upper_min_depend_of
Vgenerating
Vindependent
Ris_a_coordinate
OCompF
Ris_independent_of
OAll 68
OEx 68
#C0SP1
G0 K0 L0 M1 O4 R0 U0 V5 
Vhaving-inverse
Vadditively-closed
MSubring
Vmultiplicatively-closed
Omult_
OOne_
Vadditively-linearly-closed
Vscalar-mult-cancelable
OR_Algebra_of_BoundedFunctions
OR_Normed_Algebra_of_BoundedFunctions
#C0SP2
G0 K0 L0 M0 O4 R0 U0 V0 
OContinuousFunctions
OR_Algebra_of_ContinuousFunctions
OContinuousFunctionsNorm
OR_Normed_Algebra_of_ContinuousFunctions
#CALCUL_1
G0 K0 L0 M0 O3 R4 U0 V1 
OAnt
OSuc
Ris_tail_of
Ris_Subsequence_of
Oset_of_CQC-WFF-seq
Ris_a_correct_step
Va_proof
Ris_formal_provable_from
#CALCUL_2
G0 K0 L0 M0 O5 R0 U0 V0 
Oseq
OPer
OBegin
OImpl
OIdFinS
#CANTOR_1
G0 K0 L0 M1 O3 R0 U0 V2 
OUniCl
Vquasi_basis
OFinMeetCl
Vquasi_prebasis
Mprebasis
Othe_Cantor_set 200
#CARD_1
G0 K0 L0 M1 O5 R0 U0 V2 
O0
Vcardinal
MCardinal
Ocard 128
Onextcard 128
Vlimit_cardinal
Oalef 128
OSegm
#CARD_2
G0 K0 L0 M0 O2 R0 U0 V0 
O+` 32
O*`
#CARD_3
G0 K0 L0 M1 O11 R0 U0 V5 
VCardinal-yielding
MCardinal-Function
OCard 128
Odisjoin 128
OUnion
Oproduct 128
Opi 128
OSum 160
OProduct 128
Osproduct
Vwith_common_domain
ODOM
Oproduct" 128
Vproduct-like
Vcountable
Vdenumerable
Oproj 128
#CARD_5
G0 K0 L0 M1 O2 R0 U0 V2 
MAleph
Ocf
O-powerfunc_of
Vregular
Virregular
#CARD_FIL
G0 K0 L0 M3 O6 R5 U0 V7 
MFilter
Odual
MIdeal
Ris_multiplicative_with
Ris_additive_with
Ris_complete_with
Vuniform
Vprincipal
Vbeing_ultrafilter
OExtend_Filter
OFilters
OFrechet_Filter
OFrechet_Ideal
RGCH
Vinaccessible
Vstrong_limit
Vstrongly_inaccessible
Vmeasurable
Opredecessor
MInf_Matrix
Ris_Ulam_Matrix_of
#CARD_FIN
G0 K0 L0 M0 O2 R0 U0 V0 
OChoose
OCard_Intersection
#CARD_LAR
G0 K0 L0 M0 O2 R4 U0 V4 
Ris_unbounded_in
Ris_closed_in
Ris_club_in
Vunbounded
OLBound
Vstationary
Ris_stationary_in
Olimpoints
VMahlo
Vstrongly_Mahlo
#CATALAN1
G0 K0 L0 M0 O1 R0 U0 V0 
OCatalan
#CATALAN2
G0 K0 L0 M1 O2 R0 U0 V1 
Vdominated_by_0
ODomin_0
MOMEGA
O(##)
#CATALG_1
G0 K0 L0 M2 O8 R0 U0 V1 
O-MSF
OCatSign
MSignature
MCatSignature
Ounderlay
Vdelta-concrete
Oidsym
Ohomsym
Ocompsym
OUpsilon
OPsi
#CAT_1
G1 K0 L0 M4 O4 R0 U2 V8 
GCatStr
UComp
UId
MObject
MMorphism
OHom 128
VCategory-like
MCategory
O1Cat 255
Vmonic
Vepi
Vterminal
Vinitial
MFunctor
OObj
Visomorphic
Vfull
Vfaithful
Ohom
#CAT_2
G0 K0 L0 M2 O3 R1 U0 V0 
OFunct
MFUNCTOR-DOMAIN
MSubcategory
Ris_full_subcategory_of
O?- 128
O-? 128
#CAT_3
G0 K0 L0 M2 O3 R2 U0 V2 
Ocods 128
Vretraction
Vcoretraction
Oterm 250
Oinit 250
MProjections_family
Ris_a_product_wrt
MInjections_family
Ris_a_coproduct_wrt
#CAT_4
G2 K1 L1 M2 O13 R0 U8 V4 
Vwith_finite_product
GProdCatStr
UTerminalObj
UCatProd
UProj1
UProj2
O[1] 250
O[x]
Oc1Cat 128
VCartesian
MCartesian_category
Olambda' 128
Orho 128
Orho' 128
OSwitch 128
ODelta 128
OAlpha 128
OAlpha' 128
Vwith_finite_coproduct
GCoprodCatStr
UInitial
UCoproduct
UIncl1
UIncl2
Oin1 128
Oin2 128
Oc1Cat* 128
VCocartesian
MCocartesian_category
K[$
L$]
#CAT_5
G0 K0 L0 M0 O3 R0 U0 V3 
Vwith_triple-like_morphisms
Vcategorial
VCategorial
O-SliceCat
OSliceFunctor
OSliceContraFunctor
#CFCONT_1
G0 K0 L0 M0 O0 R1 U0 V0 
Ris_continuous_on
#CFDIFF_1
G0 K0 L0 M2 O1 R0 U0 V0 
OInvShift
MC_REST
MC_LINEAR
#CFUNCDOM
G1 K0 L0 M1 O7 R0 U0 V1 
OComplexFuncAdd
OComplexFuncMult
OComplexFuncExtMult
OComplexFuncZero
OComplexFuncUnit
OCRing
GComplexAlgebraStr
OCAlgebra
VComplexAlgebra-like
MComplexAlgebra
#CFUNCT_1
G0 K0 L0 M1 O0 R0 U0 V0 
MComplex
#CHAIN_1
G0 K0 L0 M4 O4 R1 U0 V0 
MGrating
MGap
Ocells
MCell
Oinfinite-cell
Ostar
Odel
Rbounds
MGrChain
#CHORD
G0 K0 L0 M3 O2 R1 U0 V5 
O.followSet
Vminlength
Rare_adjacent
O.AdjacentSet
MAdjGraph
Vsimplicial
MVertexSeparator
Vminimal
Vchordal
Vchordless
MVertexScheme
#CIRCCMB3
G0 K0 L0 M0 O1 R0 U0 V4 
Vstabilizing
Vwith_stabilization-limit
Ostabilization-time
Vone-gate
Vwith_nonpair_inputs
#CIRCCOMB
G0 K0 L0 M2 O2 R0 U0 V4 
MGate
O1GateCircStr
Vunsplit
Vgate`1=arity
Vgate`2isBoolean
Vgate`2=den
MFinSeqLen
O1GateCircuit
#CIRCLED1
G0 K0 L0 M1 O3 R0 U0 V0 
OCircled-Family
OCir
Mcircled_Combination
OcircledComb
#CIRCTRM1
G0 K0 L0 M3 O5 R6 U0 V0 
O-CircuitStr
Othe_action_of
O-CircuitSorts
O-CircuitCharact
O-Circuit
MCompatibleValuation
Rare_equivalent_wrt
Rpreserves_inputs_of
Rform_embedding_of
Rare_similar_wrt
Rcalculates
Rspecifies
MSortMap
MOperMap
#CIRCUIT1
G0 K0 L0 M2 O4 R0 U0 V0 
MCircuit
OSet-Constants
MInputFuncs
O-th_InputValues
Odepends_on_in
Osize
#CIRCUIT2
G0 K0 L0 M0 O7 R0 U0 V1 
OFix_inp
OFix_inp_ext
OIGTree
OIGValue
OFollowing
Vstable
OInitialComp
OComputation
#CLASSES1
G0 K0 L0 M0 O4 R2 U0 V2 
Vsubset-closed
VTarski
Ris_Tarski-Class_of
OTarski-Class 200
ORank 200
Othe_transitive-closure_of 128
Othe_rank_of 200
Rare_fiberwise_equipotent
#CLASSES2
G0 K0 L0 M3 O4 R0 U0 V1 
Vuniversal
MUniverse
OFinSETS 200
OSETS 200
OUniverse_closure
MFinSet
MSet
OUNIVERSE
#CLOPBAN1
G0 K0 L0 M1 O4 R0 U0 V0 
OComplexVectSpace
OC_VectorSpace_of_LinearOperators
OC_VectorSpace_of_BoundedLinearOperators
OC_NormSpace_of_BoundedLinearOperators
MComplexBanachSpace
#CLOPBAN2
G1 K0 L0 M3 O2 R0 U0 V0 
OC_Algebra_of_BoundedLinearOperators
MComplexBLAlgebra
GNormed_Complex_AlgebraStr
OC_Normed_Algebra_of_BoundedLinearOperators
MNormed_Complex_Algebra
MComplex_Banach_Algebra
#CLOSURE1
G1 K0 L0 M3 O2 R0 U0 V0 
MMSSetOp
GMSClosureStr
OMSFull
MMSClosureSystem
MMSClosureOperator
OMSFixPoints
#CLOSURE2
G1 K0 L0 M4 O4 R2 U1 V0 
Rin'
Rc='
OBool
MSubsetFamily
MSetOp
GClosureStr
UFamily
OFull
MClosureSystem
MClosureOperator
OClOp->ClSys
OClSys->ClOp
#CLOSURE3
G0 K0 L0 M0 O3 R0 U0 V0 
Osupp
OMSUnion
OSubAlgCl
#CLVECT_1
G2 K0 L0 M2 O1 R0 U0 V2 
GCLSStruct
VComplexLinearSpace-like
OTrivial-CLSStruct
MComplexLinearSpace
GCNORMSTR
VComplexNormSpace-like
MComplexNormSpace
#COHSP_1
G0 K0 L0 M0 O8 R1 U0 V10 
OFlatCoh
OSub_of_Fin
Vc=directed
Vc=filtered
Vd.union-closed
Rincludes_lattice_of
Vunion-distributive
Vd.union-distributive
Vc=-monotone
Vcap-distributive
VU-continuous
VU-stable
VU-linear
Ograph
OTrace
OStabCoh
OLinTrace
OLinCoh
OU+
#COH_SP
G0 K0 L0 M1 O16 R0 U0 V1 
Vbinary_complete
MCoherence_Space
OWeb
OCohSp
OCSp
OFuncsC
OMapsC
OCDom
OCCod
OCComp
OCId
OCohCat
OToler
OToler_on_subsets
OTOL
OFuncsT
OMapsT
OTolCat
#COLLSP
G1 K0 L0 M2 O0 R0 U1 V0 
MRelation3
GCollStr
UCollinearity
MCollSp
#COMBGRAS
G1 K0 L0 M1 O2 R0 U2 V5 
MPartialLinearSpace
OG_
Vclique
Vmaximal_clique
VSTAR
VTOP
GIncProjMap
Upoint-map
Uline-map
Vincidence_preserving
Oincprojmap
#COMMACAT
G0 K0 L0 M0 O4 R0 U0 V0 
OcommaObjs
OcommaMorphs
OcommaComp
Ocomma
#COMPACT1
G0 K0 L0 M0 O1 R0 U0 V6 
Vrelatively-compact
Vpre-compact
Vliminally-compact
Vlocally-relatively-compact
Vlocally-closed/compact
Vcompactification
OOne-Point_Compactification
#COMPLEX1
G0 K1 L1 M0 O4 R0 U0 V0 
ORe 128
O0c 128
O1r 128
K|.
L.|
Oabs 150
#COMPLEX2
G0 K0 L0 M0 O1 R0 U0 V0 
Oangle
#COMPLFLD
G0 K0 L0 M0 O1 R0 U0 V0 
OF_Complex
#COMPLSP1
G0 K0 L0 M0 O3 R0 U0 V0 
Oabscomplex 128
OComplexOpenSets
Othe_Complex_Space
#COMPL_SP
G0 K0 L0 M0 O2 R0 U0 V1 
Vcountably_compact
Owell_dist
OWellSpace
#COMPTRIG
G0 K0 L0 M1 O1 R0 U0 V0 
OArg
MCRoot
#COMPTS_1
G0 K0 L0 M0 O1 R0 U0 V1 
VHausdorff
O1TopSp
#COMPUT_1
G0 K0 L0 M0 O11 R1 U0 V10 
Vto-naturals
Vlen-total
Vwith_the_same_arity
OHFuncs
Ris_primitive-recursively_expressed_by
Oprimrec
Vcomposition_closed
Vprimitive-recursion_closed
Vprimitive-recursively_closed
OPrimRec
Vprimitive-recursive
Oinitial-funcs
OPR-closure
Ocomposition-closure
OPrimRec-Approximation
Vnullary
Vunary
Vternary
O(1,2)->(1,?,2)
O[!]
O[^]
O[pred]
#COMSEQ_1
G0 K0 L0 M1 O0 R0 U0 V0 
MComplex_Sequence
#COMSEQ_3
G0 K0 L0 M0 O1 R0 U0 V0 
O#N 120
#CONAFFM
G0 K0 L0 M0 O0 R0 U0 V7 
Vsatisfying_DES
Vsatisfying_AH
Vsatisfying_3H
Vsatisfying_ODES
Vsatisfying_LIN
Vsatisfying_LIN1
Vsatisfying_LIN2
#CONLAT_1
G2 K0 L0 M4 O10 R4 U3 V4 
Vquasi-empty
GContextStr
UInformation
MFormalContext
MAttribute
Ris-connected-with
Ris-not-connected-with
OObjectDerivation
OAttributeDerivation
Ophi
Opsi
Vco-Galois
GConceptStr
UExtent
UIntent
Vconcept-like
MFormalConcept
Vco-universal
OConcept-with-all-Objects
OConcept-with-all-Attributes
MSet-of-FormalConcepts
Ris-SubConcept-of
Ris-SuperConcept-of
OB-carrier
OB-meet
OB-join
OConceptLattice
#CONLAT_2
G0 K0 L0 M0 O3 R0 U0 V0 
Ogamma
OContext
ODualHomomorphism
#CONMETR
G0 K0 L0 M0 O0 R0 U0 V8 
Vsatisfying_OPAP
Vsatisfying_PAP
Vsatisfying_MH1
Vsatisfying_MH2
Vsatisfying_TDES
Vsatisfying_SCH
Vsatisfying_OSCH
Vsatisfying_des
#CONMETR1
G0 K0 L0 M0 O0 R0 U0 V6 
Vsatisfying_minor_Scherungssatz
Vsatisfying_major_Scherungssatz
Vsatisfying_Scherungssatz
Vsatisfying_indirect_Scherungssatz
Vsatisfying_minor_indirect_Scherungssatz
Vsatisfying_major_indirect_Scherungssatz
#CONNSP_1
G0 K0 L0 M0 O1 R3 U0 V0 
Rare_separated
Rare_joined
Ris_a_component_of
OComponent_of 128
#CONNSP_2
G0 K0 L0 M1 O1 R1 U0 V1 
Ma_neighborhood
Ris_locally_connected_in
Vlocally_connected
OqComponent_of 128
#CONNSP_3
G0 K0 L0 M1 O1 R0 U0 V0 
Ma_union_of_components
ODown
#CONVEX1
G0 K0 L0 M0 O2 R0 U0 V1 
Vconvex
OConvex-Family
Oconv
#CONVEX2
G0 K0 L0 M1 O0 R0 U0 V0 
MConvex_Combination
#CONVEX3
G0 K0 L0 M0 O1 R0 U0 V1 
OConvexComb
Vcone
#CONVEX4
G0 K0 L0 M1 O5 R0 U0 V0 
MC_Linear_Combination
OZeroCLC
OC_LinComb
OC_LCAdd
OC_LCMult
OLC_CLSpace
#CONVFUN1
G0 K0 L0 M0 O5 R0 U0 V0 
OAdd_in_Prod_of_RLS
OMult_in_Prod_of_RLS
OProd_of_RLS
ORLS_Real
Oepigraph
#CQC_LANG
G0 K0 L0 M2 O2 R0 U0 V0 
MSubstitution
OSubst
OCQC-WFF 254
MCQC-variable_list
#CQC_SIM1
G0 K0 L0 M0 O10 R2 U0 V0 
ONEGATIVE
OCON
OUNIVERSAL
OATOMIC
OQuantNbr
OSepFunc
ONBI
Oindex 128
OSepVar
Ris_Sep-closed_on
OSepQuadruples 100
Rare_similar
#CQC_THE1
G0 K0 L0 M0 O4 R3 U0 V2 
Vbeing_a_theory
OCn
OProof_Step_Kinds
Ris_a_correct_step_wrt
Ris_a_proof_wrt
OEffect
OTAUT
R|-
Vvalid
#CQC_THE3
G0 K0 L0 M0 O0 R2 U0 V0 
R|-|
Ris_an_universal_closure_of
#CSSPACE
G1 K0 L0 M1 O7 R0 U0 V1 
Othe_set_of_ComplexSequences
OC_id
OCZeroseq
OLinear_Space_of_ComplexSequences
Othe_set_of_l2ComplexSequences
GCUNITSTR
VComplexUnitarySpace-like
MComplexUnitarySpace
Ocl_scalar
OComplex_l2_Space
#CSSPACE3
G0 K0 L0 M0 O3 R0 U0 V0 
Othe_set_of_l1ComplexSequences
Ocl_norm
OComplex_l1_Space
#CSSPACE4
G0 K0 L0 M0 O7 R0 U0 V0 
Othe_set_of_BoundedComplexSequences
OComplex_linfty_norm
OComplex_linfty_Space
OComplexBoundedFunctions
OC_VectorSpace_of_BoundedFunctions
OComplexBoundedFunctionsNorm
OC_NormSpace_of_BoundedFunctions
#DECOMP_1
G0 K0 L0 M1 O20 R0 U0 V19 
Malpha-set
Vsemi-open
Vpre-open
Vpre-semi-open
Vsemi-pre-open
OsInt
OpInt
OalphaInt
OpsInt
OspInt
O^alpha
OSO
OPO
OSPO
OPSO
OD(c,alpha)
OD(c,p)
OD(c,s)
OD(c,ps)
OD(alpha,p)
OD(alpha,s)
OD(alpha,ps)
OD(p,sp)
OD(p,ps)
OD(sp,ps)
Vs-continuous
Vp-continuous
Valpha-continuous
Vps-continuous
Vsp-continuous
V(c,alpha)-continuous
V(c,s)-continuous
V(c,p)-continuous
V(c,ps)-continuous
V(alpha,p)-continuous
V(alpha,s)-continuous
V(alpha,ps)-continuous
V(p,ps)-continuous
V(p,sp)-continuous
V(sp,ps)-continuous
#DICKSON
G0 K0 L0 M0 O7 R1 U0 V3 
Vweakly-ascending
Vquasi_ordered
O<=E
O\~
Omin-classes
Ris_Dickson-basis_of
VDickson
Omindex
ODickson-bases
ONATOrd
OOrderedNAT
#DIFF_1
G0 K1 L1 M1 O9 R0 U0 V1 
OfD
ObD
OcD
Oforward_difference
Ofdif
Obackward_difference
Obdif
Ocentral_difference
Ocdif
K[!
L!]
VSequence-yielding
MSeq_Sequence
#DILWORTH
G0 K0 L0 M4 O4 R0 U0 V5 
MClique
MStableSet
Vwith_finite_clique#
Oclique#
Vwith_finite_stability#
Ostability#
Ominimals
Omaximals
VClique-wise
MClique-partition
VStableSet-wise
MColoring
Vstrong-chain
#DIRAF
G0 K0 L0 M2 O2 R2 U0 V1 
Olambda
OLambda
RMid
RLIN
VAffinSpace-like
MAffinSpace
MAffinPlane
#DIRORT
G0 K0 L0 M1 O0 R1 U0 V6 
R'//'
VOriented_Orthogonality_Space-like
MOriented_Orthogonality_Space
Vbach_transitive
Vright_transitive
Vleft_transitive
VEuclidean_like
VMinkowskian_like
#DIST_1
G0 K0 L0 M1 O12 R2 U0 V0 
Owhole_event
Oevent_pick
Ofrequency
OFDprobability
OFDprobSEQ
R-are_prob_equivalent
OFinseq-EQclass
Odistribution_family
OGenProbSEQ
Odistribution
OfreqSEQ
MdistProbFinS
Ris_uniformly_distributed
Ouniform_distribution
OUniform_FDprobSEQ
#DTCONSTR
G0 K0 L0 M3 O12 R0 U0 V3 
OTS
OPeanoNat
Vwith_terminals
Vwith_nonterminals
Vwith_useful_nonterminals
MTerminal
MNonTerminal
MSubtreeSeq
Oplus-one
OPN-to-NAT
OPNsucc
ONAT-to-PN
OTerminalString
OPreTraversal
OPostTraversal
OTerminalLanguage
OPreTraversalLanguage
OPostTraversalLanguage
#DYNKIN
G0 K0 L0 M1 O4 R0 U0 V1 
OseqIntersection
Vintersection_stable
Odisjointify
MDynkin_System
Ogenerated_Dynkin_System
ODynSys
#ENDALG
G0 K0 L0 M0 O6 R0 U0 V0 
OUAEnd
OUAEndComp
OUAEndMonoid
OMSAEnd
OMSAEndComp
OMSAEndMonoid
#ENS_1
G0 K0 L0 M0 O10 R0 U0 V1 
OMaps 128
Oid$
Vsurjective
OfDom 128
OfCod 128
OfComp 128
OfId 128
OEns 128
Ohom?- 128
Ohom-? 128
Ohom?? 128
#ENTROPY1
G0 K0 L0 M0 O7 R1 U0 V0 
Rhas_onlyone_value_in
OVec2DiagMx
OMx2FinS
OFinSeq_log
OInfor_FinSeq_of
OEntropy
OEntropy_of_Joint_Prob
OEntropy_of_Cond_Prob
#EQREL_1
G0 K0 L0 M5 O6 R0 U0 V1 
Onabla
MTolerance
MEquivalence_Relation
O"\/"
OClass
Ma_partition
OEqClass
OSmallestPartition
MFamily-Class
Vpartition-membered
MPart-Family
OIntersection
#EQUATION
G0 K0 L0 M1 O3 R0 U0 V0 
OSuperAlgebraSet
OTermAlg
OEquations
MEqualSet
#EUCLID
G0 K1 L1 M0 O6 R0 U0 V0 
Oabsreal
O0*
OPitag_dist
OEuclid
OTOP-REAL
O0.REAL
K|[
L]|
#EUCLIDLP
G0 K0 L0 M0 O3 R1 U0 V0 
Oline_of_REAL
Odist_v
Oplane_of_REAL
Rare_coplane
#EUCLID_3
G0 K0 L0 M0 O13 R2 U0 V0 
Ocpx2euc
Oeuc2cpx
OTriangle
Oclosed_inside_of_triangle
Oinside_of_triangle
Ooutside_of_triangle
Oplane
Rare_lindependent2
Rare_ldependent2
Otricord1
Otricord2
Otricord3
Otrcmap1
Otrcmap2
Otrcmap3
#EUCLID_4
G0 K0 L0 M0 O1 R0 U0 V0 
OTPn2Rn
#EUCLID_5
G0 K1 L1 M0 O1 R0 U0 V0 
O<X>
K|{
L}|
#EUCLID_6
G0 K0 L0 M0 O2 R0 U0 V0 
Othe_area_of_polygon3
Othe_perimeter_of_polygon3
#EUCLID_7
G0 K0 L0 M1 O4 R0 U0 V5 
VR-orthogonal
VR-normal
VR-orthonormal
Vorthogonal_basis
Vlinear_manifold
OL_Span
Oaccum
OProjFinSeq
ORN_Base
MOrthogonal_Basis
#EUCLID_8
G0 K0 L0 M0 O5 R0 U0 V0 
O<e1>
O<e2>
O<e3>
OVFunc
OVFuncdiff
#EUCLMETR
G0 K0 L0 M0 O0 R0 U0 V2 
VEuclidean
VHomogeneous
#EULER_1
G0 K0 L0 M0 O1 R0 U0 V0 
OEuler 128
#E_SIEC
G1 K0 L0 M2 O30 R0 U2 V2 
GG_Net
Uentrance
Uescape
VGG
Mgg_net
VEE
Me_net
Oempty_e_net
OTempty_e_net
OPempty_e_net
OPsingle_e_net
OTsingle_e_net
OPTempty_e_net
Oe_Places
Oe_Transitions
Oe_Flow
Oe_places
Oe_transitions
Oe_pre
Oe_post
Oe_shore
Oe_prox
Oe_flow
Oe_support
Oe_entrance
Oe_escape
Oe_stanchion
Oe_circulation
Oe_adjac
Os_transitions
Os_places
Os_carrier
Os_enter
Os_exit
Os_prox
Os_pre
Os_post
#FACIRC_1
G0 K0 L0 M0 O13 R1 U0 V4 
Vpair
Vwith_pair
Vwithout_pairs
Vnonpair-yielding
Oor3
Ris_stable_at
O2GatesCircStr
O2GatesCircOutput
O2GatesCircuit
OBitAdderOutput
OBitAdderCirc
OMajorityIStr
OMajorityStr
OMajorityICirc
OMajorityOutput
OMajorityCirc
OBitAdderWithOverflowStr
OBitAdderWithOverflowCirc
#FACIRC_2
G0 K0 L0 M0 O6 R0 U0 V0 
OSingleMSS
OSingleMSA
O-BitAdderStr
O-BitAdderCirc
O-BitMajorityOutput
O-BitAdderOutput
#FCONT_1
G0 K0 L0 M0 O0 R1 U0 V1 
Ris_continuous_in
VLipschitzian
#FCONT_2
G0 K0 L0 M0 O0 R0 U0 V1 
Vuniformly_continuous
#FDIFF_1
G0 K0 L0 M2 O2 R2 U0 V4 
Vconvergent_to_0
VREST-like
MREST
Vlinear
MLINEAR
Ris_differentiable_in
Odiff
Ris_differentiable_on
O`|
Vdifferentiable
#FDIFF_3
G0 K0 L0 M0 O2 R4 U0 V0 
Ris_Lcontinuous_in
Ris_Rcontinuous_in
Ris_right_differentiable_in
Ris_left_differentiable_in
OLdiff
ORdiff
#FF_SIEC
G0 K0 L0 M0 O18 R0 U0 V0 
OPTempty_f_net
OTempty_f_net
OPempty_f_net
OTsingle_f_net
OPsingle_f_net
Oempty_f_net
Of_enter
Of_exit
Of_prox
Of_flow
Of_places
Of_transitions
Of_pre
Of_post
Of_entrance
Of_escape
Of_circulation
Of_adjac
#FIB_FUSC
G0 K0 L0 M0 O3 R0 U0 V0 
OFib_Program
OFusc'
OFusc_Program
#FIB_NUM
G0 K0 L0 M0 O2 R0 U0 V0 
Otau
Otau_bar
#FIB_NUM2
G0 K0 L0 M0 O5 R0 U0 V0 
OFIB
OEvenNAT
OOddNAT
OEvenFibs
OOddFibs
#FIB_NUM3
G0 K0 L0 M0 O2 R0 U0 V0 
OLucas
OGenFib
#FILEREC1
G0 K0 L0 M1 O0 R1 U0 V0 
MFile
Ris_a_record_of
#FILTER_0
G0 K1 L1 M1 O2 R1 U0 V1 
K<.
L.)
Vimplicative
MI_Lattice
Olatt 128
Oequivalence_wrt
Rare_equivalence_wrt
#FILTER_1
G0 K0 L0 M0 O2 R0 U0 V0 
O/\/ 128
OLattRel 128
#FILTER_2
G0 K1 L1 M0 O0 R1 U0 V0 
K(.
L.>
Ris_max-ideal
#FINSEQOP
G0 K0 L0 M0 O1 R1 U0 V1 
Ris_an_inverseOp_wrt
Vhaving_an_inverseOp
Othe_inverseOp_wrt
#FINSEQ_1
G0 K1 L1 M2 O6 R0 U0 V4 
OSeg 128
VFinSequence-like
MFinSequence
Olen 128
K<*
L*>
O<*> 254
VFinSubsequence-like
MFinSubsequence
OSgm 128
OSeq 128
O[*]
V-long
VFinSequence-membered
#FINSEQ_2
G0 K0 L0 M3 O3 R0 U0 V0 
Oidseq 128
O|->
MFinSequenceSet
MFinSequence-DOMAIN
MTuple
O-tuples_on 128
#FINSEQ_3
G0 K0 L0 M0 O1 R0 U0 V0 
ODel
#FINSEQ_4
G0 K0 L0 M0 O4 R2 U0 V0 
Ris_one-to-one_at
Rjust_once_values
O<- 100
O.. 100
O-| 32
O|-- 32
#FINSEQ_5
G0 K0 L0 M0 O4 R0 U0 V0 
O-:
O:-
ORev 128
OIns 128
#FINSEQ_6
G0 K0 L0 M0 O1 R0 U0 V1 
Vcircular
ORotate
#FINSEQ_8
G0 K0 L0 M0 O7 R5 U0 V0 
Osmid
Oovlpart
Oovlcon
Oovlldiff
Oovlrdiff
Rseparates_uniquely
Ris_substring_of
Ris_preposition_of
Ris_postposition_of
Oinstr
Oaddcr
Ris_terminated_by
#FINSET_1
G0 K0 L0 M0 O0 R0 U0 V4 
Vfinite
Vinfinite
Vfinite-yielding
Vcentered
#FINSOP_1
G0 K0 L0 M0 O2 R0 U0 V0 
O"**" 48
Ofindom
#FINSUB_1
G0 K0 L0 M1 O1 R0 U0 V4 
Vcup-closed
Vcap-closed
Vdiff-closed
VpreBoolean
OFin 128
MFinite_Subset
#FINTOPO2
G1 K0 L0 M0 O14 R0 U1 V3 
OP_1
OP_2
OP_0
OP_A
OP_e
GFMT_Space_Str
UBNbd
OU_FMT
ONeighSp
VFo_filled
O^Fodelta
O^Fob
O^Foi
O^Fos
O^Fon
O^Fodel_i
O^Fodel_o
VFo_open
VFo_closed
#FINTOPO3
G0 K0 L0 M0 O5 R1 U0 V0 
O^d
OFcl
OFint
OFinf
OFdfl
Rare_mutually_symmetric
#FINTOPO4
G0 K0 L0 M0 O4 R1 U0 V0 
Ris_continuous
ONbdl1
OFTSL1
ONbdc1
OFTSC1
#FINTOPO5
G0 K0 L0 M0 O4 R0 U0 V0 
ONbdl2
OFTSL2
ONbds2
OFTSS2
#FINTOPO6
G0 K0 L0 M0 O0 R1 U0 V1 
Ris_minimum_path_in
Vinv_continuous
#FIN_TOPO
G0 K0 L0 M0 O13 R0 U0 V1 
OU_FT
OSinglRel
OFT{0}
Vfilled
O^delta
O^deltai
O^deltao
O^i
O^b
O^s
O^n
O^f
O^fb
O^fi
#FLANG_1
G0 K0 L0 M0 O1 R0 U0 V0 
OLex 255
#FLANG_3
G0 K0 L0 M0 O1 R0 U0 V0 
O|^..
#FRECHET
G0 K0 L0 M0 O2 R1 U0 V3 
OBalls
Vfirst-countable
Ris_convergent_to
VFrechet
Vsequential
OREAL?
#FRECHET2
G0 K0 L0 M0 O1 R0 U0 V0 
OCl_Seq
#FREEALG
G0 K0 L0 M0 O10 R0 U0 V2 
Vdisjoint_with_NAT
Vwithout_zero
Ooper
ODTConUA
OFreeOpNSG
OFreeOpSeqNSG
OFreeUnivAlgNSG
OFreeGenSetNSG
OFreeOpZAO
OFreeOpSeqZAO
OFreeUnivAlgZAO
OFreeGenSetZAO
#FSCIRC_1
G0 K0 L0 M0 O9 R0 U0 V0 
OBitSubtracterOutput
OBitSubtracterCirc
OBorrowIStr
OBorrowStr
OBorrowICirc
OBorrowOutput
OBorrowCirc
OBitSubtracterWithBorrowStr
OBitSubtracterWithBorrowCirc
#FSCIRC_2
G0 K0 L0 M0 O4 R0 U0 V0 
O-BitSubtracterStr
O-BitSubtracterCirc
O-BitBorrowOutput
O-BitSubtracterOutput
#FSM_1
G3 K0 L0 M1 O12 R6 U3 V2 
GFSM
UTran
UInitS
MState
O-succ_of
O-admissible
R-leads_to
Ris_admissible_for
Oleads_to_under
GMealy-FSM
UOFun
GMoore-FSM
O-response
Ris_similar_to
R-are_equivalent
R-equivalent
O-eq_states_EqR
O-eq_states_partition
Ofinal_states_partition
O-succ_class
O-class_response
Othe_reduction_of
R-are_isomorphic
Vreduced
Vaccessible
OaccessibleStates
O-Mealy_union
#FSM_2
G2 K0 L0 M0 O2 R3 U1 V1 
OGEN
Vcalculating_type
Ris_accessible_via
GSM_Final
UFinalS
Rleads_to_final_state_of
GMoore-SM_Final
O-TwoStatesMooreSM
Ris_result_of
#FSM_3
G2 K0 L0 M0 O4 R0 U0 V0 
O_bool
Gsemiautomaton
Oleft-Lang
Gautomaton
Oright-Lang
Ochop
#FTACELL1
G0 K0 L0 M0 O24 R0 U0 V0 
OBitFTA0Str
OBitFTA0Circ
OBitFTA0CarryOutput
OBitFTA0AdderOutputI
OBitFTA0AdderOutputP
OBitFTA0AdderOutputQ
OBitFTA1Str
OBitFTA1Circ
OBitFTA1CarryOutput
OBitFTA1AdderOutputI
OBitFTA1AdderOutputP
OBitFTA1AdderOutputQ
OBitFTA2Str
OBitFTA2Circ
OBitFTA2CarryOutput
OBitFTA2AdderOutputI
OBitFTA2AdderOutputP
OBitFTA2AdderOutputQ
OBitFTA3Str
OBitFTA3Circ
OBitFTA3CarryOutput
OBitFTA3AdderOutputI
OBitFTA3AdderOutputP
OBitFTA3AdderOutputQ
#FUNCOP_1
G0 K0 L0 M0 O6 R0 U0 V1 
O--> 16
O[:] 80
O[;] 80
VFunction-yielding
O.-->
OIFEQ
O:-> 128
#FUNCSDOM
G1 K0 L0 M2 O8 R0 U0 V1 
ORealFuncAdd
ORealFuncMult
ORealFuncExtMult
ORealFuncZero
ORealFuncUnit
ORealVectSpace
ORRing
MRing
GAlgebraStr
ORAlgebra
VAlgebra-like
MAlgebra
#FUNCTOR0
G2 K0 L0 M2 O1 R1 U2 V9 
Mbifunction
VCovariant
VContravariant
MMSUnTrans
GBimapStr
UObjectMap
Vcoreflexive
GFunctorStr
UMorphMap
OMorph-Map
Vid-preserving
Vcomp-preserving
Vcomp-reversing
Vcovariant
Vcontravariant
Vinjective
Rare_anti-isomorphic
#FUNCTOR2
G0 K0 L0 M0 O1 R0 U0 V0 
Oidt
#FUNCT_1
G0 K0 L0 M1 O2 R0 U0 V5 
VFunction-like
MFunction
O. 100
Vone-to-one
Vconstant
Othe_value_of
Vfunctional
V-compatible
#FUNCT_2
G0 K0 L0 M2 O2 R0 U0 V3 
Vquasi_total
OFuncs 128
Vonto
Vbijective
MPermutation
O/* 128
MFUNCTION_DOMAIN
#FUNCT_3
G0 K0 L0 M0 O3 R0 U0 V0 
Ochi 128
Oincl 128
Odelta 128
#FUNCT_4
G0 K1 L1 M0 O2 R0 U0 V0 
O+*
K|:
L:|
O+~
#FUNCT_5
G0 K0 L0 M0 O7 R0 U0 V0 
Ocurry 128
Ouncurry 128
Ocurry' 128
Ouncurry' 128
Oop0 110
Oop1 110
Oop2 110
#FUNCT_6
G0 K0 L0 M0 O5 R0 U0 V0 
OSubFuncs 128
Odoms 128
Orngs 128
OFrege
Ocommute
#FUNCT_7
G0 K0 L0 M1 O8 R1 U0 V1 
OIn
Requal_outside
Ocompose
Oapply
Ofirstdom
Olastrng
VFuncSeq-like
MFuncSequence
Oiter
OSwap
Ofollowed_by
#FUNCT_8
G0 K0 L0 M0 O1 R2 U0 V4 
Vsymmetrical
Vwith_symmetrical_domain
Vquasi_even
Ris_even_on
Vquasi_odd
Ris_odd_on
Osignum
#FUNCT_9
G0 K0 L0 M0 O0 R0 U0 V2 
V-periodic
Vperiodic
#FUZZY_1
G0 K0 L0 M1 O4 R0 U0 V0 
MMembership_Func
O1_minus
OEMF
OUMF
Oab_difMF
#FUZZY_2
G0 K0 L0 M1 O2 R0 U0 V0 
MRMembership_Func
OZmf
OUmf
#FUZZY_4
G0 K0 L0 M0 O2 R0 U0 V0 
Oconverse
OImf
#FVSUM_1
G0 K0 L0 M0 O3 R0 U0 V0 
Omultfield
Odiffield
O"*"
#GATE_1
G0 K0 L0 M0 O42 R0 U0 V0 
ONOT1
OAND2
OOR2
OXOR2
OEQV2
ONAND2
ONOR2
OAND3
OOR3
OXOR3
OMAJ3
ONAND3
ONOR3
OAND4
OOR4
ONAND4
ONOR4
OAND5
OOR5
ONAND5
ONOR5
OAND6
OOR6
ONAND6
ONOR6
OAND7
OOR7
ONAND7
ONOR7
OAND8
OOR8
ONAND8
ONOR8
OMODADD2
OADD1
OCARR1
OADD2
OCARR2
OADD3
OCARR3
OADD4
OCARR4
#GATE_5
G0 K0 L0 M0 O21 R0 U0 V0 
OMULT210
OMULT211
OMULT212
OMULT213
OMULT310
OMULT311
OMULT312
OMULT313
OMULT314
OMULT321
OMULT322
OMULT323
OMULT324
OCLAADD1
OCLACARR1
OCLAADD2
OCLACARR2
OCLAADD3
OCLACARR3
OCLAADD4
OCLACARR4
#GCD_1
G0 K0 L0 M3 O6 R5 U0 V1 
Ris_associated_to
Ris_not_associated_to
OClasses
MAm
MAmpleSet
ONF
Vgcd-like
MgcdDomain
Rare_canonical_wrt
Rare_co-prime
Rare_normalized_wrt
Oadd1
Oadd2
Omult1
Omult2
#GENEALG1
G0 K0 L0 M2 O2 R0 U0 V0 
MGene-Set
OGA-Space
MIndividual
Ocrossover
#GEOMTRAP
G1 K0 L0 M3 O3 R1 U0 V4 
Rare_DTr_wrt
ODTrapezium
OMidPoint
GAfMidStruct
ODTrSpace
VMidOrdTrapSpace-like
MMidOrdTrapSpace
VOrdTrapSpace-like
MOrdTrapSpace
VTrapSpace-like
MTrapSpace
VRegular
#GFACIRC1
G0 K0 L0 M0 O52 R0 U0 V0 
Oinv1
Obuf1
Oand2c
Oxor2c
OGFA0CarryIStr
OGFA0CarryICirc
OGFA0CarryStr
OGFA0CarryCirc
OGFA0CarryOutput
OGFA0AdderStr
OGFA0AdderCirc
OGFA0AdderOutput
OBitGFA0Str
OBitGFA0Circ
OBitGFA0CarryOutput
OBitGFA0AdderOutput
OGFA1CarryIStr
OGFA1CarryICirc
OGFA1CarryStr
OGFA1CarryCirc
OGFA1CarryOutput
OGFA1AdderStr
OGFA1AdderCirc
OGFA1AdderOutput
OBitGFA1Str
OBitGFA1Circ
OBitGFA1CarryOutput
OBitGFA1AdderOutput
OGFA2CarryIStr
OGFA2CarryICirc
OGFA2CarryStr
OGFA2CarryCirc
OGFA2CarryOutput
OGFA2AdderStr
OGFA2AdderCirc
OGFA2AdderOutput
OBitGFA2Str
OBitGFA2Circ
OBitGFA2CarryOutput
OBitGFA2AdderOutput
OGFA3CarryIStr
OGFA3CarryICirc
OGFA3CarryStr
OGFA3CarryCirc
OGFA3CarryOutput
OGFA3AdderStr
OGFA3AdderCirc
OGFA3AdderOutput
OBitGFA3Str
OBitGFA3Circ
OBitGFA3CarryOutput
OBitGFA3AdderOutput
#GFACIRC2
G0 K0 L0 M0 O8 R0 U0 V0 
O-BitGFA0Str
O-BitGFA0Circ
O-BitGFA0CarryOutput
O-BitGFA0AdderOutput
O-BitGFA1Str
O-BitGFA1Circ
O-BitGFA1CarryOutput
O-BitGFA1AdderOutput
#GLIB_000
G0 K0 L0 M10 O31 R6 U0 V12 
MGraphStruct
OVertexSelector
OEdgeSelector
OSourceSelector
OTargetSelector
O_GraphSelectors
Othe_Vertices_of
Othe_Edges_of
Othe_Source_of
Othe_Target_of
V[Graph-like]
M_Graph
OcreateGraph
O.set 160
O.strict
RJoins
RDJoins
RSJoins
RDSJoins
Vloopless
Vnon-multi
Vnon-Dmulti
Vsimple
VDsimple
O.order() 160
O.size() 160
O.edgesInto 160
O.edgesOutOf 160
O.edgesInOut 160
O.edgesBetween 160
O.edgesDBetween 160
MSubgraph
Vspanning
R==
R!=
MinducedSubgraph
MremoveVertex
MremoveVertices
MremoveEdge
MremoveEdges
MVertex
O.edgesIn() 160
O.edgesOut() 160
O.edgesInOut() 160
O.adj 160
O.inDegree() 160
O.outDegree() 160
O.degree() 160
O.inNeighbors() 160
O.outNeighbors() 160
O.allNeighbors() 160
Visolated
Vendvertex
VGraph-yielding
Vhalting
O.Lifespan() 160
O.Result() 160
MGraphSeq
Vnon-trivial
#GLIB_001
G0 K0 L0 M8 O22 R1 U0 V4 
MVertexSeq
MEdgeSeq
MWalk
O.walkOf 160
O.first() 160
O.last() 160
O.vertexAt 160
O.reverse() 160
O.append 160
O.cut 160
O.remove 160
O.addEdge 160
O.vertexSeq() 160
O.edgeSeq() 160
O.vertices() 160
O.edges() 160
O.length() 160
O.find 160
O.rfind 160
Ris_Walk_from
VTrail-like
VPath-like
Vvertex-distinct
VCycle-like
MTrail
MDWalk
MDTrail
MDPath
MSubwalk
O.allWalks() 160
O.allTrails() 160
O.allPaths() 160
O.allDWalks() 160
O.allDTrails() 160
O.allDPaths() 160
#GLIB_002
G0 K0 L0 M0 O4 R1 U0 V3 
Vacyclic
Ris_DTree_rooted_at
O.reachableFrom 160
O.reachableDFrom 160
VComponent-like
O.componentSet() 160
O.numComponents() 160
Vcut-vertex
#GLIB_003
G0 K0 L0 M28 O12 R0 U0 V11 
OWeightSelector
OELabelSelector
OVLabelSelector
V[Weighted]
V[ELabeled]
V[VLabeled]
MWGraph
MEGraph
MVGraph
MWEGraph
MWVGraph
MEVGraph
MWEVGraph
Othe_Weight_of
Othe_ELabel_of
Othe_VLabel_of
Vweight-inheriting
Velabel-inheriting
Vvlabel-inheriting
MWSubgraph
MESubgraph
MVSubgraph
MWESubgraph
MWVSubgraph
MEVSubgraph
MWEVSubgraph
MinducedWSubgraph
MinducedESubgraph
MinducedVSubgraph
MinducedWESubgraph
MinducedWVSubgraph
MinducedEVSubgraph
MinducedWEVSubgraph
Vreal-weighted
Vnonnegative-weighted
Vreal-elabeled
Vreal-vlabeled
Vreal-WEV
O.weightSeq() 160
O.cost() 160
O.labeledE() 160
O.labelEdge 160
O.labelVertex 160
O.labeledV() 160
MWGraphSeq
MEGraphSeq
MVGraphSeq
MWEGraphSeq
MWVGraphSeq
MEVGraphSeq
MWEVGraphSeq
#GLIB_004
G0 K0 L0 M5 O13 R2 U0 V1 
Ris_mincost_DTree_rooted_at
Ris_mincost_DPath_from
O.min_DPath_cost 160
OWGraphSelectors
O.allWSubgraphs() 160
MDIJK:Labeling
ODIJK:NextBestEdges 160
ODIJK:Step 160
ODIJK:Init 160
MDIJK:LabelingSeq
ODIJK:CompSeq 160
ODIJK:SSSP 160
MPRIM:Labeling
OPRIM:NextBestEdges 160
OPRIM:Init 160
OPRIM:Step 160
MPRIM:LabelingSeq
OPRIM:CompSeq 160
OPRIM:MST 160
Vmin-cost
MminimumSpanningTree
#GLIB_005
G0 K0 L0 M4 O12 R5 U0 V1 
Vnatural-weighted
MFF:ELabeling
Rhas_valid_flow_from
O.flow 160
Rhas_maximum_flow_from
MAP:VLabeling
Ris_forward_edge_wrt
Ris_backward_edge_wrt
Ris_augmenting_wrt
OAP:NextBestEdges 160
OAP:Step 160
MAP:VLabelingSeq
OAP:CompSeq 160
OAP:FindAugPath 160
OAP:GetAugPath 160
O.flowSeq
O.tolerance
OFF:PushFlow
OFF:Step
MFF:ELabelingSeq
OFF:CompSeq
OFF:MaxFlow
#GOBOARD1
G0 K0 L0 M1 O2 R1 U0 V4 
OX_axis 255
OY_axis 255
VX_equal-in-line
VY_equal-in-column
VY_increasing-in-line
VX_increasing-in-column
MGo-board
Ris_sequence_on
#GOBOARD2
G0 K0 L0 M0 O2 R0 U0 V0 
OGoB 128
OIncr 128
#GOBOARD4
G0 K0 L0 M0 O0 R1 U0 V0 
Rlies_between
#GOBOARD5
G0 K0 L0 M1 O5 R0 U0 V2 
Ov_strip
Oh_strip
Ocell
Vs.c.c.
Vstandard
Mspecial_circular_sequence
Oright_cell
Oleft_cell
#GOBOARD9
G0 K0 L0 M0 O2 R0 U0 V0 
OLeftComp
ORightComp
#GOBRD10
G0 K0 L0 M0 O0 R2 U0 V0 
Rare_adjacent1
Rare_adjacent2
#GOBRD13
G0 K0 L0 M0 O3 R3 U0 V0 
OValues
Ofront_right_cell
Ofront_left_cell
Rturns_right
Rturns_left
Rgoes_straight
#GOEDELCP
G0 K0 L0 M0 O3 R0 U0 V2 
Vnegation_faithful
Vwith_examples
OExCl
OEx-bound_in
OEx-the_scope_of
#GRAPHSP
G0 K0 L0 M0 O14 R6 U0 V0 
O:=
Orepeat
OOuterVx
OLifeSpan
Owhile_do
OXEdge
OWeight
OUnusedVx
OUsedVx
OArgmin
Ofindmin
Onewpathcost
RhasBetterPathAt
ORelax
Requal_at
Ris_vertex_seq_at
Ris_simple_vertex_seq_at
Ris_oriented_edge_seq_of
Ris_Input_of_Dijkstra_Alg
ODijkstraAlgorithm
#GRAPH_1
G1 K0 L0 M6 O6 R3 U2 V2 
GMultiGraphStruct
USource
UTarget
MEdge
MGraph
Ocod 128
Ris_sum_of
Voriented
Rjoins
Rare_incident
MPath
MOrientedPath
Vcyclic
MCycle
MOrientedCycle
OVerticesCount
OEdgesCount
OEdgesIn
OEdgesOut
ODegree
#GRAPH_2
G0 K0 L0 M0 O5 R4 U0 V2 
O-cut
O^'
VTwoValued
VAlternating
O-VSet
Ris_vertex_seq_of
Ralternates_vertices_in
Overtex-seq
Omin_at
Ris_non_decreasing_on
Ris_split_at
#GRAPH_3
G0 K0 L0 M0 O8 R0 U0 V1 
OEdges_In
OEdges_Out
OEdges_At
OAddNewEdge
O-CycleSet
OCatCycles
O-PathSet
OExtendCycle
VEulerian
#GRAPH_4
G0 K0 L0 M0 O3 R3 U0 V1 
Rorientedly_joins
Rare_orientedly_incident
O-SVSet
O-TVSet
Ris_oriented_vertex_seq_of
Ooriented-vertex-seq
VSimple
#GRAPH_5
G0 K0 L0 M0 O6 R6 U0 V0 
Overtices
Ris_orientedpath_of
OOrientedPaths
Ris_acyclicpath_of
OAcyclicPaths
OReal>=0
Ris_weight>=0of
Ris_weight_of
ORealSequence
Ocost
Ris_shortestpath_of
RislongestInShortestpath
#GRCAT_1
G1 K0 L0 M4 O11 R1 U1 V3 
OMorphs
Ocat
OZeroMap
GGroupMorphismStr
UFun
Ofun
OZERO 128
VGroupMorphism-like
MGroupMorphism
VGroup_DOMAIN-like
MGroup_DOMAIN
VGroupMorphism_DOMAIN-like
MGroupMorphism_DOMAIN
MMapsSet
RGO
OGroupObjects
OGroupCat
OAbGroupObjects
OAbGroupCat
OMidOpGroupObjects
OMidOpGroupCat
#GRNILP_1
G0 K0 L0 M0 O1 R0 U0 V0 
Othe_normal_subgroups_of
#GROEB_1
G0 K0 L0 M0 O2 R5 U0 V0 
Omultiples
Ris_Groebner_basis_wrt
Ris_Groebner_basis_of
ODivOrder
Ris_monic_wrt
Ris_reduced_wrt
Ris_autoreduced_wrt
#GROEB_2
G0 K0 L0 M0 O1 R5 U0 V0 
Rare_disjoint
Rare_non_disjoint
OS-Poly
Ris_MonomialRepresentation_of
Ris_Standard_Representation_of
Rhas_a_Standard_Representation_of
#GROEB_3
G0 K0 L0 M0 O3 R0 U0 V0 
OUpper_Support
OLower_Support
OLow
#GROUP_1
G0 K0 L0 M1 O4 R0 U0 V4 
Vunital
VGroup-like
MGroup
O1_
Oinverse_op 124
Opower 124
Vbeing_of_order_0
Oord 128
Vunity-preserving
#GROUP_10
G0 K0 L0 M1 O10 R4 U0 V1 
Vbeing_left_operation
MLeftOperation
Othe_left_translation_of
Othe_left_operation_of
Othe_subsets_of_card
Othe_extension_of_left_translation_of
Othe_extension_of_left_operation_of
Othe_strict_stabilizer_of
Ris_fixed_under
Othe_fixed_points_of
Rare_conjugated_under
Othe_orbit_of
Othe_orbits_of
Ris_p-group_of_prime
Ris_Sylow_p-subgroup_of_prime
Othe_sylow_p-subgroups_of_prime
#GROUP_2
G0 K0 L0 M1 O5 R0 U0 V0 
MSubgroup
O(1). 128
Ocarr 128
OLeft_Cosets 128
ORight_Cosets 128
OIndex 128
#GROUP_3
G0 K0 L0 M0 O3 R2 U0 V0 
OSubgroups 124
Rare_conjugated
Rare_not_conjugated
Ocon_class 124
ONormalizator 123
#GROUP_4
G0 K0 L0 M0 O3 R0 U0 V1 
Ogr 124
Vmaximal
OPhi 124
Olattice 124
#GROUP_5
G0 K0 L0 M0 O2 R0 U0 V0 
Ocommutators 124
Ocenter 124
#GROUP_6
G0 K0 L0 M1 O7 R0 U0 V0 
OCosets 148
OCosOp 148
O./. 100
MHomomorphism
O1: 148
Onat_hom 148
OKer 148
OImage 148
#GROUP_7
G0 K0 L0 M1 O0 R0 U0 V1 
VmultMagma-yielding
MmultMagma-Family
#GROUP_8
G0 K0 L0 M0 O1 R0 U0 V0 
ODouble_Cosets
#GROUP_9
G1 K0 L0 M4 O6 R2 U1 V4 
MAction
Ris_stable_under_the_action_of
Othe_stable_subset_generated_by
GHGrWOpStr
Uaction
MGroupWithOperators
MStableSubgroup
Othe_stable_subgroups_of
OCosAc
Vhomomorphic
Othe_stable_subgroup_of
Vcomposition_series
MCompositionSeries
Vstrictly_decreasing
Vjordan_holder
Othe_series_of_quotients_of
Rare_equivalent_under
Othe_schreier_series_of
#GRSOLV_1
G0 K0 L0 M0 O0 R0 U0 V1 
Vsolvable
#GR_CY_1
G0 K0 L0 M0 O2 R0 U0 V0 
OINT.Group
O@'
#GR_CY_3
G0 K0 L0 M0 O1 R0 U0 V2 
VSafe
VSophie_Germain
OMersenne
#HAHNBAN
G0 K0 L0 M3 O0 R0 U0 V5 
MFunctional
Vsubadditive
Vpositively_homogeneous
Vsemi-homogeneous
Vabsolutely_homogeneous
V0-preserving
MBanach-Functional
Mlinear-Functional
#HAHNBAN1
G0 K1 L1 M2 O10 R0 U0 V1 
K[**
L**]
Oi_FC
O0Functional
MRFunctional
VReal_homogeneous
O0RFunctional
MSemi-Norm
ORealVS
OprojRe
OprojIm
ORtoC
OCtoR
Oi-shift
OprodReIm
#HALLMAR1
G0 K0 L0 M2 O1 R1 U0 V1 
OCut
Ris_a_system_of_different_representatives_of
VHall
MReduction
MSinglification
#HAUSDORF
G0 K0 L0 M0 O1 R0 U0 V0 
OHausDist
#HELLY
G0 K0 L0 M2 O3 R0 U0 V1 
OmaxPrefix
M_Tree
M_Subtree
O.pathBetween 96
OMiddleVertex
Vwith_Helly_property
#HENMODEL
G0 K0 L0 M1 O2 R0 U0 V2 
VConsistent
VInconsistent
OHCar
MHenkin_interpretation
OvalH
#HERMITAN
G0 K0 L0 M3 O6 R0 U0 V6 
Vcmplxhomogeneous
Mantilinear-Functional
OQcFunctional
VcmplxhomogeneousFAF
Vhermitan
VdiagRvalued
VdiagReR+0valued
Msesquilinear-Form
Mhermitan-Form
Osignnorm
Oquasinorm
ORQ*Form
OQ*Form
Vpositivediagvalued
OScalarForm
#HEYTING1
G0 K0 L0 M0 O6 R0 U0 V0 
OAtom 110
Opair_diff 110
O=>> 30
Opseudo_compl 110
OStrongImpl 110
OSUB 110
#HEYTING2
G0 K0 L0 M0 O1 R0 U0 V0 
OInvolved
#HEYTING3
G0 K0 L0 M0 O5 R0 U0 V0 
OSubstPoset
OPFArt
OPFCrt
OPFBrt
OPFDrt
#HIDDEN
G0 K0 L0 M0 O0 R2 U0 V1 
R<>
Rin
Vstrict
#HILBASIS
G0 K0 L0 M0 O7 R0 U0 V0 
Obag_extend
OUnitBag
O1_1
Ominlen
Omonomial
Oupm
Ompu
#HILBERT1
G0 K0 L0 M1 O3 R0 U0 V6 
Vwith_VERUM
Vwith_implication
Vwith_conjunction
Vwith_propositional_variables
VHP-closed
OHP-WFF
MHP-formula
VHilbert_theory
OCnPos
OHP_TAUT
#HILBERT2
G0 K0 L0 M0 O2 R0 U0 V0 
Oprop
OHP-Subformulae
#HILBERT3
G0 K0 L0 M1 O2 R0 U0 V2 
MSetValuation
OSetVal
OPerm
Vcanonical
Vpseudo-canonical
#HOMOTHET
G0 K0 L0 M0 O0 R1 U0 V0 
Ris_Sc
#HURWITZ
G0 K0 L0 M0 O5 R0 U0 V1 
OCoeff
Odeg
Orpoly
Oqpoly
VHurwitz
OF*
#IDEAL_1
G0 K0 L0 M5 O6 R0 U0 V6 
Vadd-closed
Vleft-ideal
Vright-ideal
MRightIdeal
MLeftIdeal
Oadd|
Omult|
OGr
MLinearCombination
MLeftLinearCombination
MRightLinearCombination
O-Ideal
O-LeftIdeal
O-RightIdeal
Vfinitely_generated
VNoetherian
VPID
#IDEA_1
G0 K0 L0 M0 O19 R1 U0 V0 
Ris_expressible_by
OADD_MOD 128
ONEG_N 128
ONEG_MOD 128
OChangeVal_1 128
OChangeVal_2 128
OMUL_MOD 128
OINV_MOD 128
OIDEAoperationA 128
OIDEAoperationB 128
OIDEAoperationC 128
OMESSAGES 128
OIDEA_P 128
OIDEA_Q 128
OIDEA_P_F 128
OIDEA_Q_F 128
OIDEA_PS 128
OIDEA_QS 128
OIDEA_PE 128
OIDEA_QE 128
#INCPROJ
G0 K0 L0 M1 O3 R0 U0 V4 
OProjectiveLines
OProj_Inc
OIncProjSp_of
Vpartial
Vup-2-dimensional
Vup-3-rank
MIncProjSp
V3-dimensional
#INCSP_1
G2 K0 L0 M4 O2 R1 U6 V10 
GIncProjStr
UPoints
ULines
UInc
GIncStruct
UPlanes
UInc2
UInc3
MPOINT
MLINE
MPLANE
Ron
Vplanar
Vwith_non-trivial_lines
Vup-2-rank
Vwith_non-empty_planes
Vwith_<=1_plane_per_3_pts
Vwith_lines_inside_planes
Vwith_planes_intersecting_in_2_pts
Vup-3-dimensional
Vinc-compatible
VIncSpace-like
MIncSpace
OLine 15
OPlane 15
#INDEX_1
G0 K0 L0 M5 O4 R0 U0 V3 
VCategory-yielding
MManySortedCategory
OObjs
OMphs
VCategory-yielding_on_first
VFunction-yielding_on_second
MManySortedFunctor
MIndexing
MTargetCat
McoIndexing
O-functor
O-indexing_of
#INSTALG1
G0 K0 L0 M1 O0 R0 U0 V0 
MSubsignature
#INTEGR10
G0 K0 L0 M0 O7 R4 U0 V1 
Ris_right_ext_Riemann_integrable_on
Ris_left_ext_Riemann_integrable_on
Oext_right_integral
Oext_left_integral
Ris_+infty_ext_Riemann_integrable_on
Ris_-infty_ext_Riemann_integrable_on
Oinfty_ext_right_integral
Oinfty_ext_left_integral
Vinfty_ext_Riemann_integrable
Oinfty_ext_integral
Oexp*-
OOne-sided_Laplace_transform
#INTEGR15
G0 K0 L0 M2 O1 R0 U0 V0 
Mmiddle_volume
Omiddle_sum
Mmiddle_volume_Sequence
#INTEGR1C
G0 K0 L0 M1 O1 R0 U0 V1 
OR2-to-C
VC1-curve-like
MC1-curve
#INTEGRA1
G0 K0 L0 M1 O13 R0 U0 V4 
Vclosed-interval
MDivision
Odivs
Odivset
Oupper_volume
Olower_volume
Oupper_sum
Olower_sum
Oupper_sum_set
Olower_sum_set
Vupper_integrable
Vlower_integrable
Oupper_integral
Olower_integral
Vintegrable
Ointegral
Oindx
OPartSums
#INTEGRA2
G0 K0 L0 M1 O0 R0 U0 V0 
MDivSequence
#INTEGRA4
G0 K0 L0 M0 O0 R1 U0 V0 
Rdivide_into_equal
#INTEGRA5
G0 K1 L1 M0 O0 R1 U0 V0 
Ris_integrable_on
K['
L']
#INTEGRA7
G0 K0 L0 M0 O1 R1 U0 V0 
OIntegralFuncs
Ris_integral_of
#INTEGRA8
G0 K0 L0 M0 O1 R0 U0 V0 
OCst
#INTEGRA9
G0 K2 L2 M0 O0 R1 U0 V0 
K|||(
L)|||
Ris_orthogonal_with
K||..
L..||
#INTERVA1
G0 K0 L0 M1 O11 R0 U0 V1 
OInter
MIntervalSet
O_/\_
O_\/_
O``2 80
Vordered
O_\_
OIntervalSets
OInterLatt
ORS
ORoughSets
ORSLattice
OERS
#INTPRO_1
G0 K0 L0 M1 O10 R0 U0 V10 
Vwith_FALSUM
Vwith_int_implication
Vwith_int_conjunction
Vwith_int_disjunction
Vwith_int_propositional_variables
Vwith_modal_operator
VMC-closed
OMC-wff
MMC-formula
ONes
VIPC_theory
OCnIPC
OIPC-Taut
Oneg
OIVERUM
VCPC_theory
OCnCPC
OCPC-Taut
VS4_theory
OCnS4
OS4-Taut
#INT_1
G0 K2 L2 M1 O3 R1 U0 V1 
Vinteger
MInteger
Rare_congruent_mod
K[\
L/]
K[/
L\]
Ofrac 140
Odiv 32
Omod 32
#INT_2
G0 K0 L0 M0 O1 R0 U0 V1 
Ogcd 32
Vprime
#INT_3
G0 K0 L0 M2 O2 R0 U0 V1 
OINT.Ring
Oabsint
VEuclidian
MEuclidianRing
MDegreeFunction
#INT_4
G0 K0 L0 M0 O1 R1 U0 V0 
OCong
Ris_CRS_of
#INT_5
G0 K0 L0 M0 O2 R1 U0 V0 
OPoly-INT
Ris_quadratic_residue_mod
OLege
#INT_6
G0 K0 L0 M2 O1 R0 U0 V2 
Vmultiplicative-trivial
VChinese_Remainder
MCR_Sequence
MCR_coefficients
Oto_int
#INT_7
G0 K0 L0 M0 O3 R0 U0 V1 
Vprime-factorization-like
OSegm0
Omultint0
OZ/Z*
#IRRAT_1
G0 K0 L0 M0 O5 R0 U0 V1 
Virrational
Oaseq 250
Obseq 250
Ocseq 250
Odseq 250
Oeseq 250
#ISOCAT_1
G0 K0 L0 M1 O0 R1 U0 V0 
Ris_equivalent_with
MEquivalence
#ISOCAT_2
G0 K0 L0 M0 O2 R0 U0 V0 
Oexport
Odistribute
#ISOMICHI
G0 K0 L0 M0 O2 R1 U0 V10 
Vsupercondensed
Vsubcondensed
Vregular_open
Vregular_closed
OBound
OBorder
Rare_c=-incomparable
V1st_class
V2nd_class
V3rd_class
Vwith_1st_class_subsets
Vwith_2nd_class_subsets
Vwith_3rd_class_subsets
#JGRAPH_1
G0 K0 L0 M0 O2 R1 U0 V1 
OPGraph
OPairF
Ris_Shortcut_of
Vnodic
#JGRAPH_2
G0 K0 L0 M0 O2 R0 U0 V0 
OOut_In_Sq
OAffineMap
#JGRAPH_3
G0 K0 L0 M0 O1 R0 U0 V0 
OSq_Circ
#JGRAPH_4
G0 K0 L0 M0 O9 R0 U0 V0 
ONormF 101
OFanW
O-FanMorphW 101
OFanN
O-FanMorphN 101
OFanE
O-FanMorphE 101
OFanS
O-FanMorphS 101
#JGRAPH_6
G0 K0 L0 M0 O10 R0 U0 V0 
Orectangle
Oinside_of_rectangle
Oclosed_inside_of_rectangle
Ooutside_of_rectangle
Oclosed_outside_of_rectangle
Ocircle
Oinside_of_circle
Oclosed_inside_of_circle
Ooutside_of_circle
Oclosed_outside_of_circle
#JORDAN
G0 K0 L0 M0 O8 R0 U0 V0 
OdiffX2_1
OdiffX2_2
OdiffX1_X2_1
OdiffX1_X2_2
OProj2_1
OProj2_2
ODiskProj
ORotateCircle
#JORDAN1
G0 K0 L0 M0 O0 R0 U0 V1 
VJordan
#JORDAN10
G0 K0 L0 M0 O2 R0 U0 V0 
OUBD-Family
OBDD-Family
#JORDAN11
G0 K0 L0 M0 O3 R0 U0 V0 
OApproxIndex
OY-InitStart
OY-SpanStart
#JORDAN12
G0 K0 L0 M0 O0 R2 U0 V0 
Ris_in_general_position_wrt
Rare_in_general_position
#JORDAN13
G0 K0 L0 M0 O1 R0 U0 V0 
OSpan
#JORDAN14
G0 K0 L0 M0 O1 R0 U0 V0 
OSpanStart
#JORDAN17
G0 K0 L0 M0 O0 R1 U0 V0 
Rare_in_this_order_on
#JORDAN18
G0 K0 L0 M0 O2 R2 U0 V0 
ONorth-Bound
OSouth-Bound
R-separate
Rare_neighbours_wrt
#JORDAN19
G0 K0 L0 M0 O4 R0 U0 V0 
OUpper_Appr
OLower_Appr
ONorth_Arc
OSouth_Arc
#JORDAN1A
G0 K0 L0 M0 O1 R0 U0 V0 
OCenter
#JORDAN1E
G0 K0 L0 M0 O2 R0 U0 V0 
OUpper_Seq
OLower_Seq
#JORDAN1H
G0 K0 L0 M0 O2 R1 U0 V0 
ORealOrd
OX-SpanStart
Ris_sufficiently_large_for
#JORDAN20
G0 K0 L0 M0 O0 R6 U0 V0 
Ris_Lin
Ris_Rin
Ris_Lout
Ris_Rout
Ris_OSin
Ris_OSout
#JORDAN21
G0 K0 L0 M0 O2 R0 U0 V1 
Vwith_the_max_arc
OUMP
OLMP
#JORDAN23
G0 K0 L0 M0 O0 R0 U0 V3 
Valmost-one-to-one
Vweakly-one-to-one
Vpoorly-one-to-one
#JORDAN24
G0 K0 L0 M0 O0 R1 U0 V0 
Rrealize-max-dist-in
#JORDAN2C
G0 K0 L0 M0 O4 R2 U0 V1 
VBounded
Ris_inside_component_of
Ris_outside_component_of
OBDD
OUBD
O1*
O1.REAL
#JORDAN3
G0 K0 L0 M0 O4 R3 U0 V0 
Omid
Ris_S-Seq_joining
OL_Cut
OR_Cut
RLE
RLT
OB_Cut
#JORDAN4
G0 K0 L0 M0 O3 R3 U0 V0 
OS_Drop
Ris_a_part>_of
Ris_a_part<_of
Ris_a_part_of
OLower
OUpper
#JORDAN5C
G0 K0 L0 M0 O2 R0 U0 V0 
OFirst_Point
OLast_Point
#JORDAN5D
G0 K0 L0 M0 O16 R0 U0 V0 
Oi_s_w
Oi_n_w
Oi_s_e
Oi_n_e
Oi_w_s
Oi_e_s
Oi_w_n
Oi_e_n
On_s_w
On_n_w
On_s_e
On_n_e
On_w_s
On_e_s
On_w_n
On_e_n
#JORDAN6
G0 K0 L0 M0 O11 R0 U0 V0 
Ox_Middle
Oy_Middle
OL_Segment
OR_Segment
OSegment
OVertical_Line
OHorizontal_Line
OUpper_Arc
OLower_Arc
OLower_Middle_Point
OUpper_Middle_Point
#JORDAN8
G0 K0 L0 M0 O1 R0 U0 V0 
OGauge
#JORDAN9
G0 K0 L0 M0 O1 R0 U0 V0 
OCage
#JORDAN_A
G0 K0 L0 M1 O2 R0 U0 V0 
OEucl_dist
MSegmentation
OS-Gap
#KNASTER
G0 K0 L0 M0 O5 R0 U0 V0 
Olfp
Ogfp
O+.
O-.
OFixPoints
#KOLMOG01
G0 K0 L0 M2 O6 R1 U0 V0 
OIndep
MManySortedSigmaField
Ris_independent_wrt
MSigmaSection
OsigUn
OfutSigmaFields
OtailSigmaField
OMeetSections
OfinSigmaFields
#KURATO_1
G0 K0 L0 M0 O6 R0 U0 V2 
OKurat14Part
OKurat14Set
OKurat14ClPart
OKurat14OpPart
OKurat7Set
OKurExSet
VCl-closed
VInt-closed
#KURATO_2
G0 K0 L0 M0 O3 R0 U0 V0 
OLim_K
OLim_inf
OLim_sup
#LANG1
G2 K0 L0 M2 O7 R1 U2 V1 
GDTConstrStr
URules
GGrammarStr
UInitialSym
MSymbol
MString
OTerminals
ONonTerminals
Ris_derivable_from
OLang
OEmptyGrammar
OSingleGrammar
OIterGrammar
OTotalGrammar
Vefective
#LAPLACE
G0 K0 L0 M0 O9 R0 U0 V0 
ODelete
OReplaceCol
ORCol
ORem
OMinor
OCofactor
OMatrix_of_Cofactor
OLaplaceExpL
OLaplaceExpC
#LATTICE2
G0 K0 L0 M2 O2 R2 U0 V1 
Rabsorbs
Rdoesn't_absorb
OFinJoin 150
OFinMeet 150
MD0_Lattice
VHeyting
MH_Lattice
#LATTICE3
G0 K0 L0 M0 O3 R4 U0 V4 
OBooleLatt
OLattPOSet
O% 200
Ris_<=_than
Ris_>=_than
Vwith_suprema
Vwith_infima
Ris_less_than
Ris_greater_than
V\/-distributive
V/\-distributive
#LATTICE4
G0 K0 L0 M1 O2 R4 U0 V0 
Rpreserves_implication
Rpreserves_top
Rpreserves_bottom
Rpreserves_complement
MClosedSubset
Ofield_by
OSetImp
#LATTICE5
G0 K0 L0 M5 O13 R2 U0 V1 
OEqRelLATT
MSublattice
Rare_joint_by
Otype_of
MBiFunction
Vu.t.i.
Mdistance_function
Oalpha
Onew_set
Onew_bi_fun
ODistEsti
OConsecutiveSet
MQuadrSeq
OQuadr
OBiFun
OConsecutiveDelta
ONextSet
ONextDelta
Ris_extension_of
MExtensionSeq
OBasicDF
#LATTICE6
G0 K0 L0 M0 O2 R2 U0 V7 
Vnoetherian
Vco-noetherian
Ris-upper-neighbour-of
Ris-lower-neighbour-of
Vcompletely-meet-irreducible
Vcompletely-join-irreducible
Vco-atomic
Vsupremum-dense
Vinfimum-dense
OMIRRS
OJIRRS
#LATTICE7
G0 K0 L0 M1 O2 R1 U0 V0 
R<(1)
OJoin-IRR
OLOWER
MRing_of_sets
#LATTICE8
G0 K0 L0 M1 O7 R2 U0 V1 
Vfinitely_typed
Rhas_a_representation_of_type<=
Onew_set2
Onew_bi_fun2
OConsecutiveSet2
OQuadr2
OConsecutiveDelta2
ONextSet2
ONextDelta2
Ris_extension2_of
MExtensionSeq2
#LATTICES
G3 K0 L0 M8 O3 R1 U2 V16 
G/\-SemiLattStr
UL_meet
G\/-SemiLattStr
UL_join
GLattStr
O"/\"
Vjoin-commutative
Vjoin-associative
Vmeet-commutative
Vmeet-associative
Vmeet-absorbing
Vjoin-absorbing
VLattice-like
MLattice
Vdistributive
Vmodular
Vlower-bounded
Vupper-bounded
MD_Lattice
MM_Lattice
M0_Lattice
M1_Lattice
M01_Lattice
OBottom 129
OTop 129
Ris_a_complement_of
Vcomplemented
MC_Lattice
VBoolean
MB_Lattice
Vfinal
Vmeet-closed
Vjoin-closed
#LEXBFS
G0 K0 L0 M6 O15 R0 U0 V7 
Vwith_finite-elements
O.\/
Vnatsubset-yielding
O.incSubset
Viterative
Veventually-constant
MpreVNumberingSeq
Vvertex-numbering
MVNumberingSeq
O.PickedAt
MLexBFS:Labeling
OLexBFS:Init
OLexBFS:PickUnnumbered
OLexBFS:Update
OLexBFS:Step
MLexBFS:LabelingSeq
O``1
OLexBFS:CSeq
Vwith_property_L3
MMCS:Labeling
OMCS:Init
OMCS:PickUnnumbered
OMCS:LabelAdjacent
OMCS:Update
OMCS:Step
MMCS:LabelingSeq
OMCS:CSeq
Vwith_property_T
#LFUZZY_0
G0 K0 L0 M0 O2 R4 U0 V0 
ORealPoset
R<<=
R>>=
R~<=
R~>=
OFuzzyLattice
#LFUZZY_1
G0 K0 L0 M0 O1 R0 U0 V0 
OTrCl
#LIMFUNC1
G0 K0 L0 M0 O6 R0 U0 V8 
Oleft_open_halfline
Oleft_closed_halfline
Oright_closed_halfline
Oright_open_halfline
Vdivergent_to+infty
Vdivergent_to-infty
Vconvergent_in+infty
Vdivergent_in+infty_to+infty
Vdivergent_in+infty_to-infty
Vconvergent_in-infty
Vdivergent_in-infty_to+infty
Vdivergent_in-infty_to-infty
Olim_in+infty
Olim_in-infty
#LIMFUNC2
G0 K0 L0 M0 O2 R6 U0 V0 
Ris_left_convergent_in
Ris_left_divergent_to+infty_in
Ris_left_divergent_to-infty_in
Ris_right_convergent_in
Ris_right_divergent_to+infty_in
Ris_right_divergent_to-infty_in
Olim_left
Olim_right
#LIMFUNC3
G0 K0 L0 M0 O0 R3 U0 V0 
Ris_convergent_in
Ris_divergent_to+infty_in
Ris_divergent_to-infty_in
#LMOD_7
G0 K0 L0 M4 O5 R0 U0 V0 
MSUBMODULE_DOMAIN
MLINE_DOMAIN
Olines
MHIPERPLANE
MHIPERPLANE_DOMAIN
Ohiperplanes
OCOMPL
OADD
OLMULT
#LOPBAN_1
G0 K0 L0 M2 O11 R0 U0 V0 
OFuncAdd
OFuncExtMult
OFuncZero
MLinearOperator
OLinearOperators
OR_VectorSpace_of_LinearOperators
OBoundedLinearOperators
OR_VectorSpace_of_BoundedLinearOperators
Omodetrans
OPreNorms
OBoundedLinearOperatorsNorm
OR_NormSpace_of_BoundedLinearOperators
MRealBanachSpace
#LOPBAN_2
G1 K0 L0 M3 O5 R0 U0 V4 
OFuncMult
OFuncUnit
ORing_of_BoundedLinearOperators
OR_Algebra_of_BoundedLinearOperators
MBLAlgebra
GNormed_AlgebraStr
OR_Normed_Algebra_of_BoundedLinearOperators
MNormed_Algebra
VBanach_Algebra-like_1
VBanach_Algebra-like_2
VBanach_Algebra-like_3
VBanach_Algebra-like
MBanach_Algebra
#LOPBAN_3
G0 K0 L0 M0 O0 R0 U0 V1 
Vnorm_summable
#LOPBAN_4
G0 K0 L0 M0 O1 R1 U0 V0 
Rare_commutative
Oexp_
#LOPCLSET
G0 K0 L0 M0 O9 R0 U0 V0 
OOpenClosedSet
OT_join
OT_meet
OOpenClosedSetLatt
Oultraset
OUFilter 200
OStoneR
OStoneSpace
OStoneBLattice
#LPSPACE1
G0 K0 L0 M0 O13 R1 U0 V1 
Vmulti-closed
Omultpfunc
Omultrealpfunc
ORealPFuncZero
ORealPFuncUnit
ORLSp_PFunct
OL1_Functions
ORLSp_L1Funct
Ra.e.=
OAlmostZeroFunctions
ORLSp_AlmostZeroFunct
Oa.e-eq-class
OPre-L-Space
OL-1-Norm
OL-1-Space
#LP_SPACE
G0 K0 L0 M0 O4 R0 U0 V0 
Orto_power
Othe_set_of_RealSequences_l^
Ol_norm^
Ol_Space^
#MARGREL1
G0 K0 L0 M2 O5 R0 U0 V1 
Mrelation
Othe_arity_of 20
Mrelation_length
Orelations_on
Oempty_rel
OBOOLEAN
OALL
Vboolean-valued
#MATHMORP
G0 K0 L0 M0 O6 R0 U0 V0 
O(+) 32
O(O) 40
O(o) 40
O(.)
O(&)
O(@)
#MATRIX10
G0 K0 L0 M0 O0 R1 U0 V4 
VPositive
VNegative
VNonpositive
VNonnegative
Ris_less_or_equal_with
#MATRIX11
G0 K0 L0 M0 O5 R0 U0 V0 
O2Set
OPart_sgn
OReplaceLine
ORLine
OaddFinS
#MATRIX12
G0 K0 L0 M0 O12 R0 U0 V0 
OInterchangeLine
OScalarXLine
ORlineXScalar
OILine
OSXLine
ORLineXS
OInterchangeCol
OScalarXCol
ORcolXScalar
OICol
OSXCol
ORColXS
#MATRIX13
G0 K0 L0 M0 O3 R0 U0 V1 
OEqSegm
Vwithout_repeated_line
OFinS2MX
OMX2FinS
#MATRIX14
G0 K0 L0 M0 O1 R0 U0 V0 
OSwapDiagonal
#MATRIX15
G0 K0 L0 M0 O2 R0 U0 V0 
OSolutions_of
OSpace_of_Solutions_of
#MATRIX16
G0 K0 L0 M0 O3 R3 U0 V7 
Ris_line_circulant_about
Vline_circulant
Vfirst-line-of-circulant
Ris_col_circulant_about
Vcol_circulant
Vfirst-col-of-circulant
OLCirc
OCCirc
Vcirculant
Ris_anti-circular_about
Vanti-circular
Vfirst-line-of-anti-circular
OACirc
#MATRIXC1
G0 K0 L0 M0 O8 R0 U0 V0 
O@"
OFinSeq2Matrix
OMatrix2FinSeq
OFR2FC
OLineSum
OColSum
OSumAll
OQuadraticForm
#MATRIXJ1
G0 K0 L0 M2 O3 R0 U0 V2 
VMatrix-yielding
MFinSequence_of_Matrix
OLen
OWidth
Oblock_diagonal
VSquare-Matrix-yielding
MFinSequence_of_Square-Matrix
#MATRIXJ2
G0 K0 L0 M1 O2 R0 U0 V1 
OJordan_block
VJordan-block-yielding
MFinSequence_of_Jordan_block
Odegree_of_nilpotent
#MATRIXR1
G0 K0 L0 M0 O5 R0 U0 V0 
OMXR2MXF
OMXF2MXR
O0_Rmatrix
OColVec2Mx
OLineVec2Mx
#MATRIXR2
G0 K0 L0 M0 O2 R0 U0 V0 
O1_Rmatrix
OBase_FinSeq
#MATRIX_1
G0 K0 L0 M2 O4 R0 U0 V2 
Vtabular
MMatrix
OIndices
OCol
O-Matrices_over
Vdiagonal
MDiagonal
O-G_Matrix_over
#MATRIX_2
G0 K0 L0 M2 O7 R0 U0 V4 
O][ 100
Vupper_triangular
Vlower_triangular
MUpper_Triangular_Matrix
MLower_Triangular_Matrix
ODelCol
ODelLine
ODeleting
Vpermutational
OPermutations
OGroup_of_Perm
Vbeing_transposition
OFinOmega
#MATRIX_3
G0 K0 L0 M0 O4 R0 U0 V0 
OPath_matrix
OPath_product
ODet
Odiagonal_of_Matrix
#MATRIX_5
G0 K0 L0 M0 O3 R0 U0 V0 
OCOMPLEX2Field
OField2COMPLEX
O0_Cx
#MATRIX_6
G0 K0 L0 M0 O0 R1 U0 V1 
Ris_reverse_of
VOrthogonal
#MATRIX_7
G0 K0 L0 M0 O1 R0 U0 V0 
OIFIN
#MATRIX_8
G0 K0 L0 M0 O0 R1 U0 V4 
VIdempotent
VNilpotent
VInvolutory
VSelf_Reversible
Ris_congruent_Matrix_of
#MATRIX_9
G0 K0 L0 M0 O1 R0 U0 V0 
OPPath_product
#MATRLIN
G0 K0 L0 M1 O2 R0 U0 V0 
MOrdBasis
Olmlt
OAutMt
#MATRLIN2
G0 K0 L0 M0 O2 R0 U0 V0 
OAutEqMt
OMx2Tran
#MATROID0
G0 K0 L0 M2 O4 R3 U0 V5 
Rc/=
MSubsetFamilyStr
Vdependent
Othe_family_of
Vwith_exchange_property
MMatroid
Vfinite-membered
Vfinite-degree
OProdMatroid
OLinearlyIndependentSubsets
Ris_maximal_independent_in
ORnk
Ris_dependent_on
Vcycle
#MATRPROB
G0 K0 L0 M0 O2 R0 U0 V6 
VProbFinS
Vm-nonnegative
Vwith_sum=1
VJoint_Probability
Vwith_line_sum=1
VConditional_Probability
ORow_Marginal
OColumn_Marginal
#MCART_1
G0 K0 L0 M0 O10 R0 U0 V0 
O`1 255
O`2 255
O`3 255
O`4 255
Opr1 128
Opr2 128
O`11 255
O`12 255
O`21 255
O`22 255
#MCART_2
G0 K0 L0 M0 O5 R0 U0 V0 
O`5 255
O`6 255
O`7 255
O`8 255
O`9 255
#MEASURE1
G0 K0 L0 M5 O0 R0 U0 V1 
MMeasure
Mmeasure_zero
MN_Sub_set_fam
Vsigma-additive
MSep_Sequence
Msigma_Measure
#MEASURE2
G0 K0 L0 M1 O0 R0 U0 V0 
MN_Measure_fam
#MEASURE3
G0 K0 L0 M2 O2 R1 U0 V0 
MN_Sub_fam
Ris_complete
Mthin
OCOM
OMeasPart
#MEASURE4
G0 K0 L0 M1 O2 R0 U0 V0 
MC_Measure
Osigma_Field
Osigma_Meas
#MEASURE5
G0 K0 L0 M1 O1 R0 U0 V7 
Vopen_interval
Vclosed_interval
Vright_open_interval
Vleft_closed_interval
Vleft_open_interval
Vright_closed_interval
Vinterval
MInterval
Odiameter
#MEASURE6
G0 K0 L0 M0 O1 R0 U0 V0 
OR_EAL
#MEASURE7
G0 K0 L0 M1 O5 R0 U0 V0 
MInterval_Covering
Ovol
OSvc
OOS_Meas
OLmi_sigmaFIELD
OL_mi
#MEASURE8
G0 K0 L0 M3 O3 R0 U0 V1 
MSep_FinSequence
MSet_Sequence
MCovering
OVolume
OC_Meas
OInvPairFunc
Vcompletely-additive
#MEMBERED
G0 K0 L0 M0 O0 R0 U0 V6 
Vcomplex-membered
Vext-real-membered
Vreal-membered
Vrational-membered
Vinteger-membered
Vnatural-membered
#MEMBER_1
G0 K0 L0 M0 O5 R0 U0 V0 
O-- 32
O""
O++ 32
O**
O///
#MESFUN10
G0 K0 L0 M0 O0 R1 U0 V1 
Vuniformly_bounded
Ris_uniformly_convergent_to
#MESFUNC1
G0 K0 L0 M0 O8 R1 U0 V0 
OINT-
ORAT_with_denominator
O1.
Oeq_dom
Oless_dom
Oless_eq_dom
Ogreat_dom
Ogreat_eq_dom
Ris_measurable_on
#MESFUNC2
G0 K0 L0 M1 O0 R1 U0 V0 
MFinite_Sep_Sequence
Ris_simple_func_in
#MESFUNC3
G0 K0 L0 M0 O0 R1 U0 V0 
Rare_Re-presentation_of
#MESFUNC5
G0 K0 L0 M1 O4 R0 U0 V6 
Vnonpositive
Vwithout-infty
Vwithout+infty
MExtREAL_sequence
Vconvergent_to_finite_number
Vconvergent_to_+infty
Vconvergent_to_-infty
Ointegral'
Ointegral+
OIntegral
OIntegral_on
#MESFUNC7
G0 K0 L0 M0 O1 R0 U0 V1 
Vextreal-yielding
Omultextreal
#MESFUNC8
G0 K0 L0 M0 O0 R0 U0 V1 
Vwith_the_same_dom
#MESFUNC9
G0 K0 L0 M0 O2 R0 U0 V0 
OProjMap1
OProjMap2
#METRIC_1
G1 K0 L0 M1 O9 R0 U1 V3 
GMetrStruct
Udistance
Odist
OEmpty^2-to-zero
VReflexive
Vdiscerning
Vtriangle
MMetrSpace
Odiscrete_dist
ODiscreteSpace
Oreal_dist
ORealSpace
OBall
Ocl_Ball
OSphere
#METRIC_2
G0 K0 L0 M1 O10 R1 U0 V0 
O-neighbour
Mequivalence_class
Ris_dst
Oev_eq_1
Oev_eq_2
Oreal_in_rel
Oelem_in_rel_1
Oelem_in_rel_2
Oelem_in_rel
Oset_in_rel
Onbourdist
OEq_classMetricSpace
#METRIC_3
G0 K0 L0 M0 O9 R0 U0 V0 
Odist_cart2
Odist2
OMetrSpaceCart2
Odist_cart3
OMetrSpaceCart3
Odist3
Odist_cart4
OMetrSpaceCart4
Odist4
#METRIC_4
G0 K0 L0 M0 O14 R0 U0 V0 
Odist_cart2S
Odist2S
OMetrSpaceCart2S
Odist_cart3S
Odist3S
OMetrSpaceCart3S
Otaxi_dist2
ORealSpaceCart2
OEukl_dist2
OEuklSpace2
Otaxi_dist3
ORealSpaceCart3
OEukl_dist3
OEuklSpace3
#METRIC_6
G0 K0 L0 M0 O3 R2 U0 V0 
Obounded_metric
Ris_convergent_in_metrspace_to
Rcontains_almost_all_sequence
Odist_to_point
Osequence_of_dist
#METRIZTS
G0 K0 L0 M0 O0 R1 U0 V1 
VLindelof
Rseparates
#MIDSP_1
G1 K0 L0 M1 O8 R2 U1 V1 
GMidStr
UMIDPOINT
OExample 16
VMidSp-like
MMidSp
R@@
R##
OID 128
Ovect 32
Osetvect
Oaddvect
Ocomplvect
Ozerovect
Ovectgroup
#MIDSP_2
G1 K0 L0 M1 O3 R2 U2 V2 
Rare_associated_wrp
Ris_atlas_of
Vmidpoint_operator
OHalf
OAtlas
OMidSp.
GAtlasStr
Ualgebra
Ufunction
VATLAS-like
MATLAS
#MIDSP_3
G1 K0 L0 M1 O0 R4 U1 V1 
GReperAlgebraStr
Ureper
Vbeing_invariance
Rhas_property_of_zero_in
Ris_semi_additive_in
Ris_additive_in
Ris_alternative_in
MReperAlgebra
#MODAL_1
G0 K0 L0 M4 O5 R0 U0 V1 
ORoot
OMP-variables
MMP-variable
OMP-conectives
MMP-conective
MDOMAIN_DecoratedTree
OMP-WFF
MMP-wff
O?
Vnecessitive
#MODCAT_1
G0 K0 L0 M2 O4 R0 U0 V0 
MLeftMod_DOMAIN
MLModMorphism_DOMAIN
OLModObjects
Odom'
Ocod'
OLModCat
#MODELC_1
G2 K0 L0 M3 O50 R3 U11 V4 
Ok_id
Ok_nat
OUnivF
OCastboolean
OCastBool
Oatom.
OEX
OEG
OEU
OCTL_WFF
VCTL-formula-like
MCTL-formula
VExistNext
VExistGlobal
VExistUntill
OCastCTLformula
GKripkeStr
UWorlds
UStarts
UPossibles
ULabel
GCTLModelStr
UAssignations
UBasicAssign
UAnd
UNot
UEneXt
UEGlobal
UEUntill
MAssign
Oatomic_WFF
Ris-Evaluation-for
Ris-PreEvaluation-for
OGraftEval
OEvalSet
OCastEval
OEvalFamily
OEvaluate
O|**
Minf_path
OModelSP
OFid
ONot_0
ONot_
OEneXt_univ
OEneXt_0
OEneXt_
OEGlobal_univ
OEGlobal_0
OEGlobal_
OAnd_0
OAnd_
OEUntill_univ
OEUntill_0
OEUntill_
OF_LABEL
OLabel_
OKModel
OCTLModel
R|/=
OPrePath
OPred
OSIGMA
OTau
OFax
OSigFaxTau
OPathShift
OPathChange
OPathConc
OTransEG
OFoax
OSigFoaxTau
OTransEU
#MODELC_2
G1 K0 L0 M1 O23 R0 U4 V4 
OCastNat
O'X'
O'U'
O'R'
OLTL_WFF
VLTL-formula-like
MLTL-formula
Vnext
VUntil
VRelease
OCastLTL
GLTLModelStr
UOr
UNEXT
UUNTIL
URELEASE
Oatomic_LTL
OInf_seq
OCastSeq
ONext_univ
ONext_0
ONext_
OUntil_univ
OUntil_0
OUntil_
OOr_
ORelease_
OLTLModel
OAtomicFamily
OAtomicFunc
OAtomicAsgn
OAtomicBasicAsgn
OAtomicKai
#MODELC_3
G2 K0 L0 M0 O23 R7 U3 V3 
OLTLNew1
OLTLNew2
OLTLNext
GLTLnode
ULTLold
ULTLnew
ULTLnext
OSuccNode1
OSuccNode2
Ris_succ_of
Ris_succ1_of
Ris_succ2_of
Vfailure
Velementary
OSeed
OFinalNode
OCastNode
Ris_Finseq_for
Ris_next_of
OLength_fun
OPartial_seq
OLTLNodes
OLTLStates
Ris_succ_homomorphism
Ochosen_formula
Ochosen_succ
Ochoice_succ_func
Vneg-inner-most
GBuchiAutomaton
Ris-accepted-by
ONeg_atomic_LTL
OTran_LTL
OInitS_LTL
OFinalS_LTL
OBAutomaton
Ochosen_succ_end_num
Ochosen_next
Ochosen_run
#MOD_2
G1 K0 L0 M1 O7 R0 U2 V1 
OTrivialLMod
GLModMorphismStr
UDom
UCod
VLModMorphism-like
MLModMorphism
Oadd3
Omult3
Ocompl3
Ounit3
Ozero3
OZ3
#MOD_3
G0 K0 L0 M0 O0 R0 U0 V1 
Vbase
#MOD_4
G0 K0 L0 M2 O0 R4 U0 V12 
Vantimultiplicative
Vantilinear
Vmonomorphism
Vantimonomorphism
Vepimorphism
Vantiepimorphism
Visomorphism
Vantiisomorphism
Vendomorphism
Vantiendomorphism
Vautomorphism
Vantiautomorphism
MEndomorphism
MAutomorphism
Ris_monomorphism_wrp
Ris_epimorphism_wrp
Ris_isomorphism_wrp
Ris_automorphism_wrp
#MOEBIUS1
G0 K0 L0 M0 O6 R0 U0 V2 
Vsquare-containing
Vsquare-free
OSCNAT
OMoebius 128
ONatDivisors
OSMoebius 128
OPFactors
ORadical
#MONOID_0
G0 K0 L0 M4 O16 R0 U0 V7 
Vconstituted-Functions
Vconstituted-FinSeqs
O(*) 128
Vleft-invertible
Vright-invertible
Vleft-cancelable
Vright-cancelable
Vuniquely-decomposable
MMonoid
MMonoidalExtension
MSubStr
MMonoidalSubStr
O<REAL,+>
O<NAT,+>
O<NAT,+,0>
O<REAL,*>
O<NAT,*>
O<NAT,*,1>
O*+^
O*+^+<0>
O-concatenation
OGPFuncs
OMPFuncs
O-composition
OGFuncs
OMFuncs
OGPerms
#MONOID_1
G0 K0 L0 M1 O3 R0 U0 V0 
OMultiSet_over
MMultiset
Ofinite-MultiSet_over
O.:^2 230
#MSAFREE
G0 K0 L0 M1 O10 R0 U0 V0 
Ocoprod
MGeneratorSet
OREL
ODTConMSA
OSym 255
OFreeSort
ODenOp
OFreeOper
OFreeMSA
OFreeGen
OReverse
#MSAFREE1
G0 K0 L0 M0 O2 R0 U0 V0 
OFlatten
OSingleAlg
#MSAFREE2
G0 K0 L0 M1 O7 R0 U0 V4 
OSortsWithConstants
OInputVertices
OInnerVertices
Vwith_input_V
MInputValues
VCircuit-like
Oaction_at
OFreeEnv
OEval
Vfinitely-generated
Vmonotonic
Odepth
#MSALIMIT
G0 K0 L0 M2 O6 R0 U0 V2 
MOrderedAlgFam
MBinding
Obind
Vnormalized
ONormalized
OInvLim
VMSS-membered
OTrivialMSSign
OMSS_set
OMSS_morph
#MSATERM
G0 K0 L0 M6 O2 R1 U0 V0 
O-Terms
MTerm
MArgumentSeq
Mc-Term
O-term
MCompoundTerm
MSetWithCompoundTerm
MVariables
Ris_an_evaluation_of
#MSINST_1
G0 K0 L0 M0 O4 R0 U0 V0 
OMSSCat
OMSAlg_set
OMSAlg_morph
OMSAlgCat
#MSSCYC_1
G0 K0 L0 M0 O0 R0 U0 V4 
Vdirected_cycle-less
Vwith_directed_cycle
Vwell-founded
Vfinitely_operated
#MSSCYC_2
G0 K0 L0 M0 O4 R0 U0 V0 
OInducedEdges
OInducedSource
OInducedTarget
OInducedGraph
#MSSUBFAM
G0 K0 L0 M1 O0 R0 U0 V6 
MMSSubsetFamily
Vadditive
Vabsolutely-additive
Vmultiplicative
Vabsolutely-multiplicative
Vproperly-upper-bound
Vproperly-lower-bound
#MSUALG_1
G3 K0 L0 M2 O11 R0 U4 V1 
GManySortedSign
UArity
UResultSort
MSortSymbol
MOperSymbol
Othe_result_sort_of
Gmany-sorted
USorts
GMSAlgebra
UCharact
OArgs
OResult
ODen
Vsegmental
OMSSign
OMSSorts
OMSCharact
OMSAlg
Othe_sort_of
Othe_charact_of
O1-Alg
#MSUALG_2
G0 K0 L0 M2 O7 R0 U0 V1 
MMSSubset
Vall-with_const_op
MMSSubAlgebra
OSubSort
OMSSubSort
OGenMSAlg
OMSSub
OMSAlg_join
OMSAlg_meet
OMSSubAlLattice
#MSUALG_3
G0 K0 L0 M0 O0 R4 U0 V2 
V"1-1"
V"onto"
Ris_homomorphism
Ris_epimorphism
Ris_monomorphism
Ris_isomorphism
#MSUALG_4
G0 K0 L0 M2 O7 R0 U0 V4 
VRelation-yielding
MManySortedRelation
VMSEquivalence_Relation-like
VMSEquivalence-like
VMSCongruence-like
MMSCongruence
OQuotRes
OQuotArgs
OQuotCharact
OQuotMSAlg
OMSNat_Hom
OMSCng
OMSHomQuot
#MSUALG_5
G0 K0 L0 M0 O3 R0 U0 V0 
OEqCl
OEqRelLatt
OCongrLatt
#MSUALG_6
G0 K0 L0 M2 O5 R1 U0 V3 
Vfeasible
OTranslationRel
Ris_e.translation_of
MTranslation
Vcompatible
Vinvariant
OInvCl
OStabCl
OTRS
MEquationalTheory
OEqTh
#MSUALG_7
G0 K0 L0 M0 O1 R0 U0 V2 
V/\-inheriting
V\/-inheriting
ORealSubLatt
#MSUALG_8
G0 K0 L0 M0 O2 R0 U0 V0 
OCongrCl
OEqRelSet
#MSUALG_9
G0 K0 L0 M0 O2 R0 U0 V0 
OMpr1
OMpr2
#MSUHOM_1
G0 K0 L0 M0 O1 R0 U0 V0 
OOver
#MULTOP_1
G0 K0 L0 M2 O0 R0 U0 V0 
MTriOp
MQuaOp
#NAGATA_1
G0 K0 L0 M1 O0 R1 U0 V5 
MFamilySequence
Vsigma_discrete
Vsigma_locally_finite
Vuncountable
VBasis_sigma_discrete
VBasis_sigma_locally_finite
Ris_a_pseudometric_of
#NAGATA_2
G0 K0 L0 M0 O1 R0 U0 V0 
OPairFunc
#NATTRA_1
G0 K0 L0 M4 O4 R3 U0 V1 
Mtransformation
O`*` 120
Ris_naturally_transformable_to
Mnatural_transformation
Rare_naturally_equivalent
R~=
Mnatural_equivalence
MNatTrans-DOMAIN
ONatTrans
OFunctors
Vdiscrete
OIdCat
#NAT_1
G0 K0 L0 M2 O2 R0 U0 V0 
MNat
Omin*
Msequence
O^\
#NAT_3
G0 K0 L0 M0 O5 R0 U0 V0 
O|-count
Oprime_exponents 60
Opfexp 60
Oprime_factorization 60
Oppf 60
#NAT_5
G0 K0 L0 M0 O2 R0 U0 V0 
OEXP
OEuler_phi
#NAT_LAT
G0 K0 L0 M2 O9 R0 U0 V0 
Ohcflat
Olcmlat
ONat_Lattice
O0_NN
O1_NN
ONATPLUS
MNatPlus
Ohcflatplus
Olcmlatplus
ONatPlus_Lattice
MSubLattice
#NDIFF_2
G0 K0 L0 M0 O1 R1 U0 V0 
Ris_Gateaux_differentiable_in
OGateaux_diff
#NECKLACE
G0 K0 L0 M0 O4 R2 U0 V1 
Rembeds
Ris_equimorphic_to
Vparallel
O-SuccRelStr
OSymRelStr
OComplRelStr
ONecklace
#NECKLA_2
G0 K0 L0 M0 O4 R0 U0 V1 
VN-free
Ounion_of
Osum_of
Ofin_RelStr
Ofin_RelStr_sp
#NECKLA_3
G0 K0 L0 M1 O1 R0 U0 V1 
Mpath
Vpath-connected
Ocomponent
#NET_1
G1 K0 L0 M1 O11 R2 U3 V1 
GNet
UPlaces
UTransitions
UFlow
VPetri
OElements
MPnet
Rpre
Rpost
OPre
OPost
Oenter
Oexit
OPrec
OPostc
OEntr
OExt
OInput
OOutput
#NEWTON
G0 K0 L0 M1 O6 R0 U0 V0 
O|^ 90
OIn_Power
ONewton_Coeff
OSetPrimes
MPrime
OSetPrimenumber
Oprimenumber
#NFCONT_1
G0 K0 L0 M0 O0 R1 U0 V0 
Ris_Lipschitzian_on
#NFCONT_2
G0 K0 L0 M0 O0 R1 U0 V0 
Ris_uniformly_continuous_on
#NORMFORM
G0 K0 L0 M0 O5 R0 U0 V0 
OFinPairUnion 100
ODISJOINT_PAIRS 100
ONormal_forms_on 110
Omi 110
ONormForm 110
#NORMSP_1
G1 K1 L1 M1 O0 R0 U1 V1 
GNORMSTR
Unorm
K||.
L.||
VRealNormSpace-like
MRealNormSpace
#NORMSP_2
G0 K0 L0 M0 O4 R0 U0 V0 
Odistance_by_norm_of
OMetricSpaceNorm
OTopSpaceNorm
OLinearTopSpaceNorm
#NUMBERS
G0 K0 L0 M0 O6 R0 U0 V0 
ONAT 255
OREAL 255
OCOMPLEX 128
ORAT 255
OINT 255
OExtREAL
#NUMERAL1
G0 K0 L0 M0 O2 R0 U0 V0 
Ovalue
Odigits
#OPENLATT
G0 K0 L0 M0 O12 R0 U0 V0 
OTopology_of
OTop_Union
OTop_Meet
OOpen_setLatt
OF_primeSet
OStoneH 200
OStoneS
OSF_have
OSet_Union
OSet_Meet
OStoneLatt
OHTopSpace
#OPOSET_1
G0 K0 L0 M5 O3 R2 U0 V24 
Vdneg
Vinvolutive
OTrivOrthoRelStr
OTrivPoset
OTrivAsymOrthoRelStr
VDneg
VSubReFlexive
VSubIrreFlexive
VSubSymmetric
VSubAntisymmetric
VAsymmetric
VSubTransitive
VSubQuasiOrdered
VSubPreOrdered
VQuasiOrdered
VPreOrdered
VQuasiPure
MQuasiPureOrthoRelStr
VSubPartialOrdered
VPartialOrdered
VPure
MPureOrthoRelStr
VSubStrictPartialOrdered
VStrictPartialOrdered
VStrictOrdered
VOrderinvolutive
VOrderInvolutive
MPreOrthoPoset
RQuasiOrthoComplement_on
VQuasiOrthocomplemented
ROrthoComplement_on
VOrthocomplemented
MQuasiOrthoPoset
MOrthoPoset
#OPPCAT_1
G0 K0 L0 M1 O2 R0 U0 V0 
MContravariant_Functor
Oid* 128
O*id 128
#ORDERS_1
G0 K0 L0 M2 O1 R9 U0 V3 
MChoice_Function
OBOOL 122
MOrder
Vbeing_quasi-order
Vbeing_partial-order
Vbeing_linear-order
Rquasi_orders
Rpartially_orders
Rlinearly_orders
Rhas_upper_Zorn_property_wrt
Rhas_lower_Zorn_property_wrt
Ris_maximal_in
Ris_minimal_in
Ris_superior_of
Ris_inferior_of
#ORDERS_2
G1 K0 L0 M2 O4 R0 U1 V0 
GRelStr
UInternalRel
MPoset
OUpperCone 122
OLowerCone 122
OInitSegm 122
MInitial_Segm
OChains 122
#ORDERS_3
G0 K0 L0 M1 O4 R0 U0 V2 
Vdisconnected
VPOSet_set-like
MPOSet_set
OMonFuncs
OCarr
OPOSCat
OPOSAltCat
#ORDERS_4
G0 K0 L0 M0 O0 R1 U0 V0 
Rform_upper_lower_partition_of
#ORDINAL1
G0 K0 L0 M3 O4 R0 U0 V7 
Osucc 128
Vepsilon-transitive
Vepsilon-connected
Vordinal
Mnumber
MOrdinal
Vlimit_ordinal
VT-Sequence-like
MT-Sequence
Vc=-linear
OOn 128
OLim 128
Oomega 128
Vnatural
#ORDINAL2
G0 K0 L0 M1 O9 R2 U0 V3 
Olast 128
Oinf 128
Osup 200
VOrdinal-yielding
MOrdinal-Sequence
Olim_sup 128
Olim_inf 128
Ris_limes_of
Olim
Vincreasing
Vcontinuous
O+^ 32
O*^
Oexp
Ris_cofinal_with
#ORDINAL3
G0 K0 L0 M0 O3 R0 U0 V0 
O-^ 32
Odiv^ 32
Omod^ 32
#ORDINAL4
G0 K0 L0 M0 O3 R0 U0 V0 
O^
O0-element_of 128
O1-element_of 128
#ORDINAL5
G0 K0 L0 M0 O5 R0 U0 V3 
O|^|^
Vepsilon
Ofirst_epsilon_greater_than
Oepsilon_
OSum^
VCantor-component
O-exponent
VCantor-normal-form
#ORTSP_1
G0 K0 L0 M1 O0 R0 U0 V1 
VOrtSp-like
MOrtSp
#OSAFREE
G0 K0 L0 M2 O18 R0 U0 V1 
MOSGeneratorSet
Vosfree
OOSREL
ODTConOSA
OOSSym
OParsedTerms
OPTDenOp
OPTOper
OParsedTermsOSA
OLeastSort
OLeastSorts
OLCongruence
OFreeOSA
OPTClasses
OPTCongruence
OPTVars
OOSFreeGen
ONHReverse
OPTMin
MMinTerm
OMinTerms
#OSALG_1
G3 K0 L0 M4 O7 R3 U1 V3 
GOverloadedMSSign
UOverloading
GRelSortedSign
GOverloadedRSSign
Vorder-sorted
Vdiscernable
Vop-discrete
OOSSign
MOrderSortedSign
Rhas_least_args_for
Rhas_least_sort_for
Rhas_least_rank_for
OConstOSSet
MOrderSortedSet
OConstOSA
MOSAlgebra
OOSAlg
OTrivialOSA
OOperNames
MOperName
OName
#OSALG_2
G0 K0 L0 M3 O11 R0 U0 V0 
MOrderSortedSubset
MOSSubset
MOSSubAlgebra
OOSConstants
OOSCl
OOSbool
OOSSubSort
OOSMSubSort
OGenOSAlg
O"\/"_os
OOSSub
OOSAlg_join
OOSAlg_meet
OOSSubAlLattice
#OSALG_3
G0 K0 L0 M0 O0 R1 U0 V0 
Rare_os_isomorphic
#OSALG_4
G0 K0 L0 M2 O11 R0 U0 V2 
Vos-compatible
MOrderSortedRelation
MOSCongruence
OPath_Rel
Vlocally_directed
OCompClass
OOSClass
O#_os
OOSQuotRes
OOSQuotArgs
OOSQuotCharact
OQuotOSAlg
OOSNat_Hom
OOSCng
OOSHomQuot
#O_RING_1
G0 K0 L0 M0 O0 R0 U0 V13 
Vbeing_a_square
Vbeing_a_Sum_of_squares
Vbeing_a_sum_of_squares
Vbeing_a_Product_of_squares
Vbeing_a_product_of_squares
Vbeing_a_Sum_of_products_of_squares
Vbeing_a_sum_of_products_of_squares
Vbeing_an_Amalgam_of_squares
Vbeing_an_amalgam_of_squares
Vbeing_a_Sum_of_amalgams_of_squares
Vbeing_a_sum_of_amalgams_of_squares
Vbeing_a_generation_from_squares
Vgenerated_from_squares
#PARSP_1
G1 K0 L0 M2 O7 R1 U1 V1 
Oc3add
Oc3compl
MRelation4
GParStr
U4_arg_relation
R'||'
OC3
O4C3
OPRs
OPR
OMPS
VParSp-like
MParSp
#PARSP_2
G0 K0 L0 M1 O0 R3 U0 V1 
VFanodesSp-like
MFanodesSp
Ris_collinear
Rparallelogram
Rcongr
#PARTFUN1
G0 K1 L1 M1 O3 R1 U0 V1 
MPartFunc
K<:
L:>
Vtotal
OPFuncs 128
Rtolerates
OTotFuncs 128
O/. 100
#PARTFUN3
G0 K0 L0 M0 O0 R0 U0 V4 
Vpositive-yielding
Vnegative-yielding
Vnonpositive-yielding
Vnonnegative-yielding
#PARTIT1
G0 K0 L0 M0 O7 R4 U0 V0 
R'<'
R'>'
Ris_a_dependent_set_of
Ris_min_depend
OPARTITIONS
O'/\'
O'\/'
OERl
ORel
O%I
O%O
#PASCH
G0 K0 L0 M0 O0 R0 U0 V5 
Vsatisfying_Int_Par_Pasch
Vsatisfying_Ext_Par_Pasch
Vsatisfying_Gen_Par_Pasch
Vsatisfying_Ext_Bet_Pasch
Vsatisfying_Int_Bet_Pasch
#PBOOLE
G0 K1 L1 M4 O5 R3 U0 V0 
MManySortedSet
O[0] 250
Roverlaps
Rdoes_not_overlap
R[=
MManySortedFunction
MComponent
O#
O*-->
K[|
L|]
OMSFuncs
MManySortedSubset
O.:.:
#PCOMPS_1
G0 K0 L0 M0 O4 R1 U0 V3 
Vlocally_finite
Oclf
Vparacompact
OFamily_open_set
OTopSpaceMetr
Ris_metric_of
OSpaceMetr
Vmetrizable
#PCOMPS_2
G0 K0 L0 M0 O3 R0 U0 V0 
OPartUnion
ODisjointFam
OPartUnionNat
#PCS_0
G2 K1 L1 M3 O19 R1 U1 V17 
K[^
L^]
Vtransitive-yielding
Opcs-InternalRels
GTolStr
UToleranceRel
R(--)
Vpcs-tol-total
Vpcs-tol-reflexive
Vpcs-tol-irreflexive
Vpcs-tol-symmetric
OemptyTolStr
VTolStr-yielding
Vpcs-tol-reflexive-yielding
Vpcs-tol-irreflexive-yielding
Vpcs-tol-symmetric-yielding
Opcs-ToleranceRels
O^`1
O^`2
Gpcs-Str
Vpcs-compatible
Vpcs-like
Vanti-pcs-like
Opcs-total
Mpcs
Manti-pcs
Opcs-empty
Opcs-singleton
Vpcs-Str-yielding
Vpcs-yielding
Vpcs-chain-like
Mpcs-Chain
Opcs-union
OMSSet
Opcs-sum
Opcs-extension
Opcs-reverse
Opcs-times
Vpcs-self-coherent
Vpcs-self-coherent-membered
Opcs-general-power-IR
Opcs-general-power-TR
Opcs-general-power
Opcs-coherent-power
Opcs-power
#PDIFF_1
G0 K0 L0 M0 O4 R2 U0 V0 
O<>*
Oreproj
Ris_partial_differentiable_in
Opartdiff
Ris_partial_differentiable_on
O`partial|
#PDIFF_2
G0 K0 L0 M0 O3 R2 U0 V0 
OSVF1
Ris_partial_differentiable`1_on
Ris_partial_differentiable`2_on
O`partial1|
O`partial2|
#PDIFF_3
G0 K0 L0 M0 O9 R8 U0 V0 
Opdiff1
Ris_hpartial_differentiable`11_in
Ris_hpartial_differentiable`12_in
Ris_hpartial_differentiable`21_in
Ris_hpartial_differentiable`22_in
Ohpartdiff11
Ohpartdiff12
Ohpartdiff21
Ohpartdiff22
Ris_hpartial_differentiable`11_on
Ris_hpartial_differentiable`12_on
Ris_hpartial_differentiable`21_on
Ris_hpartial_differentiable`22_on
O`hpartial11|
O`hpartial12|
O`hpartial21|
O`hpartial22|
#PDIFF_4
G0 K0 L0 M0 O5 R1 U0 V0 
Ris_partial_differentiable`3_on
O`partial3|
Ograd
ODirectiondiff
Ounitvector
Ocurl
#PENCIL_1
G0 K0 L0 M2 O2 R1 U0 V12 
MBlock
Rare_collinear
Vclosed_under_lines
Vstrong
Vwith_non_trivial_blocks
Videntifying_close_blocks
Vtruly-partial
Vwithout_isolated_points
MPLS
VTopStruct-yielding
Vnon-void-yielding
Vtrivial-yielding
Vnon-Trivial-yielding
VPLS-yielding
VSegre-like
OSegre_Blocks
OSegre_Product
#PENCIL_2
G0 K0 L0 M2 O0 R1 U0 V0 
MSegre-Coset
Rare_joinable
MCollineation
#PENCIL_3
G0 K0 L0 M0 O2 R0 U0 V0 
Opermutation_of_indices 255
Ocanonical_embedding
#PENCIL_4
G0 K0 L0 M0 O9 R0 U0 V0 
Osegment
Opencil
OPencils_of
OPencilSpace
OSubspaceSet
OGrassmannSpace
OPairSet
OPairSetFamily
OVeroneseSpace
#PEPIN
G0 K0 L0 M0 O3 R0 U0 V0 
OCrypto 128
Oorder 128
OFermat 128
#PETRI
G1 K0 L0 M6 O0 R0 U2 V4 
GPT_net_Str
US-T_Arcs
UT-S_Arcs
Mplace
Mplaces
Mtransition
Mtransitions
MS-T_arc
MT-S_arc
VDeadlock-like
VWith_Deadlocks
VTrap-like
VWith_Traps
#PETRI_2
G1 K0 L0 M4 O8 R0 U2 V2 
Ocylinder0
Mthin_cylinder
Othin_cylinders
OExtcylinders
ORistcylinders
Oloc
OCylinderFunc
GColored_PT_net_Str
UColoredSet
Ufiring-rule
Voutbound
OOutbds
VColored-PT-net-like
MColored-PT-net
Mconnecting-mapping
Mconnecting-firing-rule
Osynthesis
#PNPROC_1
G0 K0 L0 M4 O7 R0 U0 V0 
Mmarking
Omultitude_of
O{$}
Ofire
MPetri_net
Mfiring-sequence
Mprocess
Obefore
Oconcur
ONeutralProcess
OElementaryProcess
#POLYALG1
G0 K0 L0 M1 O3 R0 U0 V1 
Vmix-associative
OFormal-Series
MSubalgebra
OGenAlg
OPolynom-Algebra
#POLYEQ_1
G0 K0 L0 M0 O3 R0 U0 V0 
OPolynom
OQuard
OTri
#POLYEQ_2
G0 K0 L0 M0 O1 R0 U0 V0 
OFour0
#POLYEQ_3
G0 K0 L0 M0 O1 R0 U0 V0 
O^3 254
#POLYEQ_5
G0 K0 L0 M0 O8 R0 U0 V0 
O-real-root
O1_root_of_cubic
O2_root_of_cubic
O3_root_of_cubic
O1_root_of_quartic
O2_root_of_quartic
O3_root_of_quartic
O4_root_of_quartic
#POLYFORM
G1 K0 L0 M2 O23 R0 U2 V5 
Mincidence-matrix
GPolyhedronStr
UPolytopsF
UIncidenceF
Vpolyhedron_1
Vpolyhedron_2
Vpolyhedron_3
Mpolyhedron
O-polytopes
Oeta
O-polytope-seq
Onum-polytopes
Onum-vertices
Onum-edges
Onum-faces
O-th-polytope
Oincidence-value
O-chain-space
O-chains
Oincidence-sequence
OBoundary
O-boundary
O-circuit-space
O-circuits
O-bounding-chain-space
O-bounding-chains
O-bounding-circuit-space
O-bounding-circuits
Vsimply-connected
Oalternating-f-vector
Oalternating-proper-f-vector
Oalternating-semi-proper-f-vector
Veulerian
#POLYNOM1
G0 K0 L0 M2 O3 R0 U0 V0 
OSupport
MSeries
O0_
MPolynomial
OPolynom-Ring
#POLYNOM2
G0 K0 L0 M0 O2 R0 U0 V0 
Oeval
OPolynom-Evaluation
#POLYNOM3
G0 K0 L0 M0 O5 R0 U0 V0 
OTuplesOrder
ODecomp
OprodTuples
O0_.
O1_.
#POLYNOM4
G0 K0 L0 M0 O1 R0 U0 V0 
OLeading-Monomial
#POLYNOM5
G0 K0 L0 M0 O5 R1 U0 V2 
O`^
Ris_a_root_of
Vwith_roots
Valgebraic-closed
ORoots
ONormPolynomial
OFPower
OPolynomial-Function
#POLYNOM6
G0 K0 L0 M0 O1 R0 U0 V0 
OCompress
#POLYNOM7
G0 K0 L0 M2 O2 R0 U0 V3 
Vunivariate
Vmonomial-like
MMonomial
OMonom
Ocoefficient
VConstant
MConstPoly
#POLYNOM8
G0 K0 L0 M0 O7 R1 U0 V0 
Oemb
Opow
OmConv
OaConv
Ris_primitive_root_of_degree
ODFT
OVandermonde
OVM
#POLYRED
G0 K0 L0 M0 O1 R6 U0 V0 
Rreduces_to
Ris_reducible_wrt
Ris_irreducible_wrt
Ris_in_normalform_wrt
Rtop_reduces_to
Ris_top_reducible_wrt
OPolyRedRel
#POSET_1
G0 K0 L0 M0 O10 R0 U0 V1 
OiterSet
Oiter_min
OConFuncs
OConRelat
OConPoset
Osup_func
Omin_func
Oleast_fix_point
Ofix_func
Vchain-complete
O-image
#POWER
G0 K0 L0 M0 O4 R0 U0 V0 
O-root 200
Oto_power 120
Olog 200
Onumber_e
#PRALG_1
G0 K1 L1 M1 O10 R0 U0 V4 
K[[:
L:]]
OInv 128
OTrivialOp
OTrivialOps
OTrivial_Algebra
VUniv_Alg-yielding
V1-sorted-yielding
Vequal-signature
OComSign
MManySortedOperation
Vequal-arity
OComAr
OEmptySeq
OProdOp
OProdOpSeq
OProdUnivAlg
#PRALG_2
G0 K0 L0 M1 O5 R0 U0 V0 
OCommute
MMSAlgebra-Family
OSORTS
OOPER
O?.
OOPS
#PRALG_3
G0 K0 L0 M1 O1 R0 U0 V0 
Oconst
MMSAlgebra-Class
#PRELAMB
G2 K0 L0 M5 O3 R4 U4 V8 
Gtypealg
Uleft_quotient
Uright_quotient
Uinner_product
Mtype
MPreProof
Vcorrect
Vleft
Vright
Vmiddle
Vprimitive
Rrepresents
Rdoes_not_represent
Vfree
Orepr_of
MProof
Vcut-free
Osize_w.r.t.
Ocutdeg
MModel
Gtypestr
Uderivability
R==>.
VSynTypes_Calculus-like
MSynTypes_Calculus
R<==>.
#PREPOWER
G0 K0 L0 M1 O5 R0 U0 V1 
OGeoSeq 120
O-Root 120
O#Z 120
O#Q 120
VRational_Sequence-like
MRational_Sequence
O#R 120
#PRE_FF
G0 K0 L0 M0 O2 R0 U0 V0 
OFib
OFusc
#PRE_POLY
G0 K0 L0 M1 O10 R0 U0 V2 
OFlattenSeq
OSgmX
VFinSequence-yielding
O^^
Osupport
Vfinite-support
Mbag
OBags
OEmptyBag
OBagOrder
ONatMinor
Odivisors
Odecomp
#PRE_TOPC
G1 K0 L0 M3 O1 R0 U1 V7 
GTopStruct
Utopology
VTopSpace-like
MTopSpace
MPoint
MSubSpace
OCl 128
VT_0
VT_1
VT_2
Vnormal
VT_3
VT_4
#PRGCOR_1
G0 K0 L0 M0 O2 R0 U0 V0 
Oidiv1_prg
Oidiv_prg
#PRGCOR_2
G0 K0 L0 M0 O6 R5 U0 V0 
OFS2XFS
OXFS2FS
OFS2XFS*
OXFS2FS*
Ris_an_xrep_of
OIFLGT
Oinner_prd_prg
Rscalar_prd_prg
Rvector_minus_prg
Rvector_add_prg
Rvector_sub_prg
#PROB_1
G0 K0 L0 M4 O5 R0 U0 V4 
Vcompl-closed
MField_Subset
MSetSequence
OComplement
Vnon-ascending
Vnon-descending
Vsigma-multiplicative
MSigmaField
MProbability
Osigma
Ohalfline
OFamily_of_halflines
OBorel_Sets
#PROB_2
G0 K0 L0 M0 O3 R1 U0 V1 
O@Intersection
O@Complement
Vdisjoint_valued
Rare_independent_respect_to
O.|. 110
#PROB_3
G0 K0 L0 M1 O7 R0 U0 V2 
OPartial_Intersection
OPartial_Union
OPartial_Diff_Union
O@Partial_Intersection
O@Partial_Union
O@Partial_Diff_Union
Vnon-decreasing-closed
Vnon-increasing-closed
MMonotoneClass
Omonotoneclass
#PROB_4
G0 K0 L0 M0 O4 R0 U0 V0 
OP2M
OM2P
OP_COM2M_COM
OProbPart
#PROJDES1
G0 K0 L0 M0 O0 R2 U0 V0 
Rare_coplanar
Rconstitute_a_quadrangle
#PROJPL_1
G0 K0 L0 M2 O0 R3 U0 V1 
R|'
Vconfiguration
MIncProjectivePlane
Ris_a_triangle
Ris_a_quadrangle
MQuadrangle
#PROJRED1
G0 K0 L0 M0 O1 R0 U0 V0 
OIncProj
#PROJRED2
G0 K0 L0 M1 O1 R1 U0 V0 
Rare_concurrent
OCHAIN
MProjection
#PRVECT_1
G0 K0 L0 M4 O6 R0 U0 V1 
O-Group_over
O-Mult_over
O-VectSp_over
MDomain-Sequence
MBinOps
MUnOps
VAbGroup-yielding
MGroup-Sequence
Oaddop
Ocomplop
Ozeros
#PRVECT_2
G0 K0 L0 M3 O3 R0 U0 V2 
MMultOps
VRealLinearSpace-yielding
MRealLinearSpace-Sequence
Omultop
VRealNormSpace-yielding
MRealNormSpace-Sequence
Onormsequence
Oproductnorm
#PSCOMP_1
G0 K0 L0 M1 O20 R0 U0 V3 
Vwith_max
Vwith_min
MRealMap
Vpseudocompact
OW-bound
ON-bound
OE-bound
OS-bound
OSW-corner
ONW-corner
ONE-corner
OSE-corner
OW-most
ON-most
OE-most
OS-most
OW-min
OW-max
ON-min
ON-max
OE-max
OE-min
OS-max
OS-min
#PUA2MSS1
G0 K0 L0 M1 O3 R5 U0 V0 
MIndexedPartition
O-index_of
ODomRel
OLimDomRel
Ris_partitable_wrt
Ris_exactly_partitable_wrt
Rform_morphism_between
Ris_rougher_than
Rcan_be_characterized_by
#PYTHTRIP
G0 K0 L0 M1 O0 R0 U0 V3 
Vsquare
MPythagorean_triple
Vdegenerate
Vsimplified
#PZFMISC1
G0 K0 L0 M0 O0 R1 U0 V0 
Ris_transformable_to
#QC_LANG1
G0 K0 L0 M7 O12 R0 U0 V1 
OQC-variables 128
MQC-variable
Obound_QC-variables 128
Ofixed_QC-variables 128
Ofree_QC-variables 128
OQC-pred_symbols 128
MQC-pred_symbol
O-ary_QC-pred_symbols 128
Mbound_QC-variable
Mfixed_QC-variable
Mfree_QC-variable
MQC-variable_list
VQC-closed
OQC-WFF 128
MQC-formula
O@ 128
OVERUM 128
Othe_pred_symbol_of 20
Othe_arguments_of 20
Ostill_not-bound_in 68
#QC_LANG2
G0 K0 L0 M0 O3 R0 U0 V0 
OFALSUM 68
Othe_left_disjunct_of 66
Othe_right_disjunct_of 66
#QC_LANG3
G0 K0 L0 M0 O3 R0 U0 V0 
Oa. 68
OVars 68
OFixed 68
#QC_LANG4
G0 K0 L0 M2 O4 R0 U0 V0 
Olist_of_immediate_constituents
Otree_of_subformulae
O-entry_points_in_subformula_tree_of
MSubformula
MEntry_Point_in_Subformula_Tree
Oentry_points_in_subformula_tree
#QMAX_1
G2 K0 L0 M1 O8 R2 U3 V1 
OProbabilities
GQM_Str
UObservables
UStates
UQuantum_Probability
OObs
OSts
OMeas
VQuantum_Mechanics-like
MQuantum_Mechanics
GOrthoRelStr
Ris_an_involution_in
Ris_a_Quantuum_Logic_on
OProp
OPropRel
OOrdRel
OInvRel
#QUANTAL1
G3 K0 L0 M4 O3 R0 U1 V10 
GQuantaleStr
GQuasiNetStr
Vwith_left-zero
Vwith_right-zero
Vwith_zero
Vtimes-additive
Vtimes-continuous
MQuantale
MQuasiNet
MBlikleNet
Vinflationary
Vdeflationary
Vtimes-monotone
O-r>
O-l>
Vdualizing
GGirard-QuantaleStr
Uabsurd
Vdualized
MGirard-Quantale
ONegation
#QUATERN2
G0 K0 L0 M0 O8 R0 U0 V0 
Ocompquaternion
Oaddquaternion
Odiffquaternion
Omultquaternion
Odivquaternion
Oinvquaternion
OG_Quaternion
OR_Quaternion
#QUATERNI
G0 K0 L0 M0 O9 R0 U0 V1 
OQUATERNION
Vquaternion
O<j>
O<k>
ORea
OIm1
OIm2
OIm3
O0q
O1q
#QUOFIELD
G0 K0 L0 M0 O17 R3 U0 V5 
OQ.
Opadd
Opmult
OQClass.
OQuot.
Oqadd
Oqmult
Oq0.
Oq1.
Oqaddinv
Oqmultinv
Oquotadd
Oquotmult
Oquotaddinv
Oquotmultinv
Othe_Field_of_Quotients
VRingHomomorphism
VRingEpimorphism
VRingMonomorphism
Vembedding
VRingIsomorphism
Ris_embedded_in
Ris_ringisomorph_to
OcanHom
Rhas_Field_of_Quotients_Pair
#RADIX_1
G0 K0 L0 M0 O13 R1 U0 V0 
ORadix 128
O-SD 128
ODigA 128
ODigB 128
OSubDigit 128
ODigitSD 128
OSDDec 128
ODigitDC 128
ODecSD 128
OSD_Add_Carry 128
OSD_Add_Data 128
Ris_represented_by
OAdd 128
O'+' 128
#RADIX_2
G0 K0 L0 M0 O9 R0 U0 V0 
OSubDigit2 128
ODigitSD2 128
OSDDec2 128
ODigitDC2 128
ODecSD2 128
OTable1 128
OMul_mod 128
OTable2 128
OPow_mod 128
#RADIX_3
G0 K0 L0 M0 O12 R0 U0 V0 
O-SD_Sub_S 128
O-SD_Sub 128
OSDSub_Add_Carry 128
OSDSub_Add_Data 128
ODigA_SDSub 128
OSD2SDSubDigit 128
OSD2SDSubDigitS 128
OSD2SDSub 128
ODigB_SDSub 128
OSDSub2INTDigit 128
OSDSub2INT 128
OSDSub2IntOut 128
#RADIX_4
G0 K0 L0 M0 O1 R0 U0 V0 
OSDSubAddDigit 128
#RADIX_5
G0 K0 L0 M0 O8 R0 U0 V0 
OSDMinDigit 128
OSDMin 128
OSDMaxDigit 128
OSDMax 128
OFminDigit 128
OFmin 128
OFmaxDigit 128
OFmax 128
#RADIX_6
G0 K0 L0 M0 O10 R2 U0 V0 
OM0Digit 128
OM0 128
OMmaxDigit 128
OMmax 128
OMminDigit 128
OMmin 128
Rneeds_digits_of
OMmaskDigit 128
OMmask 128
OFSDMinDigit 128
OFSDMin 128
Ris_Zero_over
#RAMSEY_1
G0 K0 L0 M0 O1 R1 U0 V0 
Ris_homogeneous_for
O||^
#RANDOM_1
G0 K0 L0 M1 O3 R0 U0 V0 
OTrivial-SigmaField
OTrivial-Probability
MReal-Valued-Random-Variable
Oexpect
#RANKNULL
G0 K0 L0 M1 O3 R0 U0 V0 
Mlinear-transformation
Oim
Orank
Onullity
#RAT_1
G0 K0 L0 M1 O0 R0 U0 V1 
Vrational
MRational
#RCOMP_1
G0 K0 L0 M1 O0 R0 U0 V3 
Vcompact
Vclosed
Vopen
MNeighbourhood
#RCOMP_3
G0 K0 L0 M2 O0 R0 U0 V0 
MIntervalCover
MIntervalCoverPts
#REALSET1
G0 K0 L0 M4 O3 R2 U0 V0 
Ris_in
MPreserv
O|| 100
Ris_Bin_Op_Preserv
MPresv
O||| 100
MDnT
O!
MOnePoint
#REALSET2
G0 K0 L0 M0 O5 R0 U0 V1 
Oadd_2
Omult_2
OdL-Z_2
VField-like
Oomf 188
Orevf 201
#REALSET3
G0 K0 L0 M0 O2 R0 U0 V0 
Oosf 199
Oovf 188
#REAL_1
G0 K0 L0 M1 O0 R0 U0 V0 
MReal
#REAL_3
G0 K0 L0 M1 O14 R0 U0 V1 
Vinteger-yielding
MInteger_Sequence
OmodSeq 110
OdivSeq 110
Oremainders_for_scf 110
Orfs 110
OSimpleContinuedFraction 110
Oscf 110
Oconvergent_numerators 110
Oconvergent_denominators 110
Oc_n 110
Oc_d 110
Oconvergents_of_continued_fractions 110
Ococf 110
ObackContinued_fraction 110
Obcf 110
#REAL_LAT
G0 K0 L0 M0 O6 R0 U0 V0 
Ominreal
Omaxreal
OReal_Lattice
Omaxfuncreal
Ominfuncreal
ORealFunc_Lattice
#REAL_NS1
G0 K0 L0 M0 O6 R0 U0 V0 
OEuclid_add
OEuclid_mult
OEuclid_norm
OREAL-NS
OEuclid_scalar
OREAL-US
#REARRAN1
G0 K0 L0 M1 O3 R0 U0 V3 
Vterms've_same_card_as_number
Vascending
Vlenght_equal_card_of_set
MRearrangmentGen
OCo_Gen
ORland 200
ORlor 200
#RECDEF_2
G0 K0 L0 M0 O12 R0 U0 V0 
O`1_3
O`2_3
O`3_3
O`1_4
O`2_4
O`3_4
O`4_4
O`1_5
O`2_5
O`3_5
O`4_5
O`5_5
#RELAT_1
G0 K0 L0 M1 O13 R0 U0 V5 
VRelation-like
MRelation
Oproj1 128
Odom 128
Oproj2 128
Orng 128
Ofield 128
O~ 128
O*
Vnon-empty
Oid 128
O| 100
O.: 100
O" 128
Vempty-yielding
OIm 128
OCoim
V-defined
V-valued
#RELAT_2
G0 K0 L0 M0 O0 R8 U0 V8 
Ris_reflexive_in
Ris_irreflexive_in
Ris_symmetric_in
Ris_antisymmetric_in
Ris_asymmetric_in
Ris_connected_in
Ris_strongly_connected_in
Ris_transitive_in
Vreflexive
Virreflexive
Vsymmetric
Vantisymmetric
Vasymmetric
Vconnected
Vstrongly_connected
Vtransitive
#RELSET_2
G0 K1 L1 M0 O1 R0 U0 V0 
K{_{
L}_}
O.:^
#REWRITE1
G0 K0 L0 M2 O2 R13 U0 V10 
O$^
MRedSequence
Rreduces
Rare_convertible_wrt
Ris_a_normal_form_wrt
Ris_a_normal_form_of
Rare_convergent_wrt
Rare_divergent_wrt
Rare_convergent<=1_wrt
Rare_divergent<=1_wrt
Rhas_a_normal_form_wrt
Onf
Vco-well_founded
Vweakly-normalizing
Vstrongly-normalizing
Rcommutes-weakly_with
Rcommutes_with
Vwith_UN_property
Vwith_NF_property
Vsubcommutative
Vconfluent
Vwith_Church-Rosser_property
Vlocally-confluent
Vcomplete
Rare_equivalent
Rare_critical_wrt
MCompletion
#REWRITE2
G0 K0 L0 M2 O2 R2 U0 V1 
VXFinSequence-yielding
O^+
Msemi-Thue-system
MThue-system
R-->.
O==>.-relation
R==>*
#REWRITE3
G1 K0 L0 M0 O1 R0 U0 V1 
Gtransition-system
Vdeterministic
Odim2
#RFINSEQ
G0 K0 L0 M0 O2 R0 U0 V0 
O/^
OMIM 128
#RFINSEQ2
G0 K0 L0 M0 O4 R0 U0 V0 
Omax_p
Omin_p
Osort_d
Osort_a
#RFUNCT_3
G0 K0 L0 M2 O5 R2 U0 V0 
Omax+ 200
Omax- 200
MPartFunc-set
MPFUNC_DOMAIN
Oaddpfunc 200
OCHI 128
Ris_common_for_dom
Ris_convex_on
OFinS 200
#RFUNCT_4
G0 K0 L0 M0 O0 R8 U0 V0 
Ris_strictly_convex_on
Ris_quasiconvex_on
Ris_strictly_quasiconvex_on
Ris_strongly_quasiconvex_on
Ris_upper_semicontinuous_in
Ris_upper_semicontinuous_on
Ris_lower_semicontinuous_in
Ris_lower_semicontinuous_on
#RINFSUP1
G0 K0 L0 M0 O2 R0 U0 V0 
Oinferior_realsequence
Osuperior_realsequence
#RINGCAT1
G1 K0 L0 M3 O2 R0 U0 V3 
GRingMorphismStr
VRingMorphism-like
MRingMorphism
VRing_DOMAIN-like
MRing_DOMAIN
VRingMorphism_DOMAIN-like
MRingMorphism_DOMAIN
ORingObjects
ORingCat
#RING_1
G0 K0 L0 M0 O1 R0 U0 V2 
Vquasi-prime
Vquasi-maximal
OQuotientRing
#RLSUB_1
G0 K0 L0 M2 O2 R0 U0 V1 
Vlinearly-closed
MSubspace
O(0). 124
O(Omega). 148
MCoset
#RLSUB_2
G0 K0 L0 M1 O3 R1 U0 V0 
OSubspaces 154
Ris_the_direct_sum_of
MLinear_Compl
OSubJoin 124
OSubMeet 124
#RLTOPSP1
G1 K0 L0 M2 O2 R0 U0 V6 
OLSeg
Vconvex-membered
Vcircled
Vcircled-membered
GRLTopStruct
Vadd-continuous
VMult-continuous
MLinearTopSpace
Otransl
Mlocal_base
Vlocally-convex
#RLVECT_1
G1 K0 L0 M2 O1 R0 U1 V4 
GRLSStruct
UMult
MVECTOR
VAbelian
Vadd-associative
Vright_zeroed
VRealLinearSpace-like
OTrivial-RLSStruct
MRealLinearSpace
#RLVECT_2
G0 K0 L0 M1 O7 R0 U0 V0 
Ovector 128
MLinear_Combination
OCarrier 128
OZeroLC 128
OLinComb 128
OLCAdd 128
OLCMult 128
OLC_RLSpace 128
#RLVECT_3
G0 K0 L0 M1 O1 R0 U0 V2 
Vlinearly-independent
Vlinearly-dependent
OLin 128
MBasis
#RLVECT_5
G0 K0 L0 M0 O2 R0 U0 V1 
Vfinite-dimensional
Odim
OSubspaces_of
#RMOD_2
G0 K0 L0 M1 O0 R0 U0 V0 
MSubmodule
#RMOD_3
G0 K0 L0 M0 O1 R0 U0 V0 
OSubmodules
#ROBBINS1
G3 K0 L0 M1 O13 R0 U1 V6 
GComplStr
UCompl
GComplLattStr
GOrthoLattStr
OTrivComplLat
OTrivOrtLat
VRobbins
VHuntington
Vjoin-idempotent
OBot 129
Vwell-complemented
MpreOrthoLattice
OCLatt
Vwith_idempotent_element
O\delta
OExpand
O_0
ODouble
O_1
O_2
O_3
O_4
O\beta
Vde_Morgan
#ROBBINS2
G0 K0 L0 M0 O0 R0 U0 V3 
Vsatisfying_DN_1
Vsatisfying_MD_1
Vsatisfying_MD_2
#ROBBINS3
G4 K0 L0 M4 O6 R0 U0 V6 
Vjoin-Associative
Vmeet-Associative
Vmeet-Absorbing
O|_|
O|^|
O"|^|"
O"|_|"
G\/-SemiLattRelStr
G/\-SemiLattRelStr
GLattRelStr
OTrivLattRelStr
GOrthoLattRelStr
OTrivCLRelStr
Vwith_Top
MOrtholattice
MRelAugmentation
MLatAugmentation
Vnaturally_sup-generated
Vnaturally_inf-generated
MCLatAugmentation
#ROBBINS4
G0 K0 L0 M1 O2 R0 U0 V2 
Vorthomodular
MOrthomodular_Lattice
VOrthomodular
OB_6
OBenzene
#ROUGHS_1
G0 K0 L0 M3 O5 R6 U0 V4 
Vwith_equivalence
Vwith_tolerance
MApproximation_Space
MTolerance_Space
OLAp
OUAp
OBndAp
Vrough
Vexact
MRoughSet
OMemberFunc
OFinSeqM
R_c=
Rc=^
R_c=^
R_=
R=^
R_=^
#RPR_1
G0 K0 L0 M2 O1 R1 U0 V0 
MEl_ev
MEvent
Oprob
Rare_independent
#RSSPACE
G0 K0 L0 M0 O13 R0 U0 V0 
Othe_set_of_RealSequences
Oseq_id
OR_id
Ol_add
Ol_mult
OZeroseq
OLinear_Space_of_RealSequences
OAdd_
OMult_
OZero_
Othe_set_of_l2RealSequences
Ol_scalar
Ol2_Space
#RSSPACE3
G0 K0 L0 M0 O3 R0 U0 V2 
Othe_set_of_l1RealSequences
Ol_norm
Ol1_Space
VCCauchy
VCauchy_sequence_by_Norm
#RSSPACE4
G0 K0 L0 M0 O7 R0 U0 V0 
Othe_set_of_BoundedRealSequences
Olinfty_norm
Olinfty_Space
OBoundedFunctions
OR_VectorSpace_of_BoundedFunctions
OBoundedFunctionsNorm
OR_NormSpace_of_BoundedFunctions
#RUSUB_4
G0 K0 L0 M0 O1 R0 U0 V2 
VAffine
OUp
VSubspace-like
#RUSUB_5
G0 K0 L0 M0 O2 R1 U0 V0 
Ris_parallel_to
OOrt_Comp
OTopUnitSpace
#RVSUM_1
G0 K1 L1 M0 O3 R1 U0 V1 
Osqrreal 128
Osqr 128
Omlt 128
Vcomplex-yielding
K|(
L)|
Rare_orthogonal
#SCMBSORT
G0 K0 L0 M0 O3 R0 U0 V0 
Obubble-sort
OBubble-Sort-Algorithm
OSorting-Function
#SCMFSA6A
G0 K0 L0 M0 O3 R0 U0 V0 
ODirected
OMacro
OInitialized
#SCMFSA6B
G0 K0 L0 M0 O1 R0 U0 V3 
OIExec
Vparaclosed
Vparahalting
Vkeeping_0
#SCMFSA6C
G0 K0 L0 M0 O1 R0 U0 V0 
OInitialize
#SCMFSA7B
G0 K0 L0 M0 O0 R3 U0 V1 
Rdoes_not_refer
Rdoes_not_destroy
Vgood
Ris_halting_on
#SCMFSA8A
G0 K0 L0 M0 O2 R1 U0 V1 
OGoto
Ris_pseudo-closed_on
Vpseudo-paraclosed
Opseudo-LifeSpan
#SCMFSA8B
G0 K0 L0 M0 O3 R0 U0 V0 
Oif=0
Oif>0
Oif<0
#SCMFSA8C
G0 K0 L0 M0 O2 R0 U0 V0 
Oloop
OTimes
#SCMFSA9A
G0 K0 L0 M0 O3 R4 U0 V1 
RProperBodyWhile=0
RWithVariantWhile=0
OExitsAtWhile=0
RProperBodyWhile>0
RWithVariantWhile>0
OExitsAtWhile>0
Von_data_only
OFusc_macro
#SCMFSA_1
G0 K0 L0 M1 O13 R0 U0 V0 
OSCM+FSA-Data-Loc
OSCM+FSA-Data*-Loc
OSCM+FSA-Memory
OSCM+FSA-Instr
OSCM+FSA-OK
MSCM+FSA-State
OSCM+FSA-Chg
Oint_addr1
Oint_addr2
Ocoll_addr1
Oint_addr3
Ocoll_addr2
OSCM+FSA-Exec-Res
OSCM+FSA-Exec
#SCMFSA_2
G0 K0 L0 M2 O8 R0 U0 V0 
OSCM+FSA
OInt-Locations
OFinSeq-Locations
MInt-Location
MFinSeq-Location
Ointloc
Oinsloc
Ofsloc
O:=len
O:=<0,...,0>
#SCMFSA_7
G0 K0 L0 M0 O2 R0 U0 V0 
OLoad
OaSeq
#SCMFSA_9
G0 K0 L0 M0 O5 R0 U0 V0 
Owhile=0
Owhile>0
Owhile<0
OStepWhile=0
OStepWhile>0
#SCMISORT
G0 K0 L0 M0 O2 R0 U0 V0 
Oinsert-sort
OInsert-Sort-Algorithm
#SCMNORM
G0 K0 L0 M2 O3 R0 U0 V0 
ONext
MpreProgram
OComput
MAutonomy
OIncrIC
#SCMPDS_1
G0 K0 L0 M1 O17 R0 U0 V0 
OSCMPDS-Instr
OSCMPDS-OK
MSCMPDS-State
OAddress_Add
Oconst_INT
OP21address
OP22const
OP31address
OP32const
OP33const
OP41address
OP42address
OP43const
OP44const
OPopInstrLoc
ORetSP
ORetIC
OSCMPDS-Exec
#SCMPDS_2
G0 K0 L0 M1 O8 R0 U0 V0 
OSCMPDS
MInt_position
ODataLoc
Oreturn
OsaveIC
O<>0_goto
O<=0_goto
O>=0_goto
OICplusConst
#SCMPDS_3
G0 K0 L0 M0 O1 R0 U0 V0 
Oinspos
#SCMPDS_4
G0 K0 L0 M0 O1 R1 U0 V1 
Ostop
Rvalid_at
Vshiftable
#SCMPDS_5
G0 K0 L0 M0 O0 R0 U0 V1 
VNo-StopCode
#SCMPDS_6
G0 K0 L0 M0 O3 R0 U0 V0 
Oif<>0
Oif<=0
Oif>=0
#SCMPDS_7
G0 K0 L0 M0 O1 R0 U0 V0 
Ofor-down
#SCMPDS_8
G0 K0 L0 M0 O1 R0 U0 V0 
ODstate
#SCMP_GCD
G0 K0 L0 M0 O4 R0 U0 V0 
Ointpos
OGBP
OSBP
OGCD-Algorithm
#SCMRING1
G0 K0 L0 M0 O2 R0 U0 V0 
Oconst_address
Oconst_value
#SCM_1
G0 K0 L0 M1 O0 R0 U0 V0 
MState-consisting
#SCM_COMP
G0 K0 L0 M1 O6 R0 U0 V0 
OSCM-AE
Mbin-term
O-Meaning_on
OSelfwork
OSCM-Compile
Od".
Omax_Data-Loc_in
#SCM_HALT
G0 K0 L0 M0 O0 R2 U0 V3 
VInitClosed
VInitHalting
VkeepInt0_1
Ris_closed_onInit
Ris_halting_onInit
#SCPINVAR
G0 K0 L0 M0 O1 R0 U0 V0 
Owhile<>0
#SCPISORT
G0 K0 L0 M0 O0 R1 U0 V0 
Ris_FinSequence_on
#SCPQSORT
G0 K0 L0 M0 O2 R0 U0 V0 
OPartition
OQuickSort
#SEMI_AF1
G0 K0 L0 M1 O2 R2 U0 V1 
VSemi_Affine_Space-like
MSemi_Affine_Space
Osum
Oopposite
Rtrap
Rqtrap
#SEQFUNC
G0 K0 L0 M1 O0 R3 U0 V0 
MFunctional_Sequence
Rcommon_on_dom
Ris_point_conv_on
Ris_unif_conv_on
#SEQM_3
G0 K0 L0 M0 O0 R0 U0 V1 
Vmonotone
#SEQ_1
G0 K0 L0 M1 O0 R0 U0 V0 
MReal_Sequence
#SEQ_2
G0 K0 L0 M0 O0 R0 U0 V1 
Vconvergent
#SEQ_4
G0 K0 L0 M0 O2 R0 U0 V0 
Oupper_bound 128
Olower_bound 128
#SERIES_1
G0 K0 L0 M0 O1 R0 U0 V2 
OPartial_Sums 250
Vsummable
Vabsolutely_summable
#SERIES_3
G0 K0 L0 M0 O1 R0 U0 V0 
OPartial_Product 250
#SETFAM_1
G0 K0 L0 M2 O6 R2 U0 V4 
Omeet 128
Ris_finer_than
Ris_coarser_than
OUNION
OINTERSECTION
ODIFFERENCE
MSubset-Family
OCOMPLEMENT
Vwith_non-empty_elements
OIntersect
Vempty-membered
Vwith_non-empty_element
MCover
Vwith_proper_subsets
#SETLIM_1
G0 K0 L0 M0 O2 R0 U0 V0 
Oinferior_setsequence
Osuperior_setsequence
#SETLIM_2
G0 K0 L0 M0 O4 R0 U0 V0 
O(/\)
O(\/)
O(\)
O(\+\)
#SETWISEO
G0 K1 L1 M0 O4 R0 U0 V1 
O{}. 150
Vhaving_a_unity
K{.
L.}
O$$ 80
OFinUnion 150
Osingleton 150
#SETWOP_2
G0 K0 L0 M0 O1 R0 U0 V0 
OfinSeg
#SFMASTR1
G0 K0 L0 M0 O10 R0 U0 V0 
ORWNotIn-seq
O-thRWNotIn
O-stRWNotIn
O-ndRWNotIn
O-rdRWNotIn
O-thNotUsed
O-stNotUsed
O-ndNotUsed
O-rdNotUsed
OFib_macro
#SFMASTR2
G0 K0 L0 M0 O4 R1 U0 V0 
Otimes
OStepTimes
RProperTimesBody
Otriv-times
OFib-macro
#SFMASTR3
G0 K0 L0 M0 O4 R1 U0 V0 
OStepForUp
RProperForUpBody
Ofor-up
OFinSeqMin
OSelection-sort
#SF_MASTR
G0 K0 L0 M0 O6 R0 U0 V2 
OUsedIntLoc
OUsedInt*Loc
Vread-only
Vread-write
OFirstNotIn
OFirstNotUsed
OFirst*NotIn
OFirst*NotUsed
#SGRAPH1
G1 K0 L0 M2 O7 R4 U1 V0 
Onat_interval
OTWOELEMENTSETS
GSimpleGraphStruct
USEdges
OSIMPLEGRAPHS
MSimpleGraph
Ris_isomorphic_to
Ris_SetOfSimpleGraphs_of
MSubGraph
Odegree
Ris_path_of
OPATHS
Ris_cycle_of
OK_
OTriangleGraph
#SHEFFER1
G3 K0 L0 M0 O4 R1 U1 V9 
Vupper-bounded'
OTop'
Vlower-bounded'
OBot'
Vdistributive'
Ris_a_complement'_of
Vcomplemented'
O`# 100
Vmeet-idempotent
GShefferStr
Ustroke
GShefferLattStr
GShefferOrthoLattStr
OTrivShefferOrthoLattStr
Vproperly_defined
Vsatisfying_Sheffer_1
Vsatisfying_Sheffer_2
Vsatisfying_Sheffer_3
#SHEFFER2
G0 K0 L0 M0 O0 R0 U0 V1 
Vsatisfying_Sh_1
#SINCOS10
G0 K0 L0 M0 O4 R0 U0 V0 
Oarcsec1
Oarcsec2
Oarccosec1
Oarccosec2
#SIN_COS
G0 K0 L0 M0 O22 R0 U0 V0 
OCHK
OProd_complex_n
OProd_real_n
O!c
OExpSeq
OrExpSeq
OCoef
OCoef_e
OExpan
OExpan_e
OAlfa
OConj
Osin
Ocos
OP_sin
OP_cos
Oexp_R
OP_dt
OP_t
Otan
Ocot
OPI
#SIN_COS2
G0 K0 L0 M0 O3 R0 U0 V0 
Osinh
Ocosh
Otanh
#SIN_COS3
G0 K0 L0 M0 O4 R0 U0 V0 
Osin_C
Ocos_C
Osinh_C
Ocosh_C
#SIN_COS4
G0 K0 L0 M0 O2 R0 U0 V0 
Ocosec
Osec
#SIN_COS5
G0 K0 L0 M0 O3 R0 U0 V0 
Ocoth
Osech
Ocosech
#SIN_COS6
G0 K0 L0 M0 O2 R0 U0 V0 
Oarcsin
Oarccos
#SIN_COS7
G0 K0 L0 M0 O8 R0 U0 V0 
Osinh"
Ocosh1"
Ocosh2"
Otanh"
Ocoth"
Osech1"
Osech2"
Ocsch"
#SIN_COS9
G0 K0 L0 M0 O2 R0 U0 V0 
Oarctan
Oarccot
#SPPOL_1
G0 K0 L0 M0 O0 R2 U0 V3 
Ris_extremal_in
Vhorizontal
Vvertical
Valternating
Rare_generators_of
#SPPOL_2
G0 K0 L0 M2 O0 R1 U0 V1 
MS-Sequence_in_R2
Rsplit
Vspecial_polygonal
MSpecial_polygon_in_R2
#SPRECT_1
G0 K0 L0 M0 O1 R0 U0 V1 
OSpStSeq
Vrectangular
#SPRECT_2
G0 K0 L0 M0 O0 R3 U0 V1 
Ris_in_the_area_of
Ris_a_h.c._for
Ris_a_v.c._for
Vclockwise_oriented
#SQUARE_1
G0 K0 L0 M0 O2 R0 U0 V0 
O^2 254
Osqrt 200
#STIRL2_1
G0 K0 L0 M0 O1 R0 U0 V1 
V"increasing
Oblock
#STRUCT_0
G5 K0 L0 M0 O1 R0 U4 V2 
G1-sorted
Ucarrier
GZeroStr
UZeroF
GOneStr
UOneF
GZeroOneStr
Vdegenerated
G2-sorted
Ucarrier'
Vvoid
ONonZero
#SUBLEMMA
G0 K0 L0 M1 O8 R0 U0 V1 
MVal_Sub
OVal_S
OCQCSub_&
VCQC-WFF-like
OCQCSub_All
OCQCSub_the_scope_of
OCQCQuant
ONEx_Val
ORSub1
ORSub2
#SUBSET_1
G0 K0 L0 M2 O3 R0 U0 V1 
MElement
MSubset
O[#] 128
O` 150
Ochoose
Vproper
#SUBSTLAT
G0 K0 L0 M0 O2 R0 U0 V0 
OSubstitutionSet
OSubstLatt
#SUBSTUT1
G0 K0 L0 M2 O25 R1 U0 V7 
OvSUB
MCQC_Substitution
OCQC_Subst
ORestrictSub
OBound_Vars
ODom_Bound_Vars
OSub_Var
ONSub
OupVar
OExpandSub
RPQSub
OQSub
VQC-Sub-closed
OQC-Sub-WFF
OSub_P
VSub_VERUM
OSub_not
OSub_&
Vquantifiable
Msecond_Q_comp
OSub_All
VSub_atomic
VSub_negative
VSub_conjunctive
VSub_universal
OSub_the_arguments_of
OSub_the_argument_of
OSub_the_left_argument_of
OSub_the_right_argument_of
OSub_the_bound_of
OSub_the_scope_of
OS_Bound
OQuant
OCQC_Sub
OCQC-Sub-WFF
#SUBSTUT2
G0 K0 L0 M1 O4 R0 U0 V0 
OSbst
OCFQ
OQScope
OQsc
MPATH
#SUB_METR
G0 K0 L0 M4 O4 R1 U0 V2 
MPseudoMetricSpace
VDiscerning
MSemiMetricSpace
MNonSymmetricMetricSpace
Vultra
MUltraMetricSpace
OSet_to_zero
OZeroSpace
Ris_between
Oopen_dist_Segment
Oclose_dist_Segment
#SUPINF_1
G0 K0 L0 M2 O4 R0 U0 V0 
MR_eal
OSetMajorant
OSetMinorant
Mbool_DOMAIN
OSUP
OINF
#SUPINF_2
G0 K0 L0 M4 O3 R1 U0 V1 
O0. 128
MDenum_Set_of_R_EAL
Vnonnegative
MPos_Denum_Set_of_R_EAL
MNum
OSer 200
MSet_of_Series
OSUM
Ris_sumable
#SYMSP_1
G1 K0 L0 M1 O2 R1 U0 V1 
GSymStr
R_|_
VSymSp-like
MSymSp
OProJ
OPProJ
#SYSREL
G0 K0 L0 M0 O1 R0 U0 V0 
OCL
#TARSKI
G0 K0 L0 M0 O1 R2 U0 V0 
Rc=
Ounion 128
Rare_equipotent
#TAXONOM1
G0 K0 L0 M2 O4 R1 U0 V0 
MClassification
MStrong_Classification
Olow_toler
Ofam_class
Rare_in_tolerance_wrt
Odist_toler
Ofam_class_metr
#TAXONOM2
G0 K0 L0 M1 O0 R0 U0 V5 
Vwith_superior
Vwith_comparable_down
Vhierarchic
MHierarchy
Vmutually-disjoint
Vwith_max's
#TAYLOR_1
G0 K0 L0 M0 O3 R0 U0 V0 
Olog_
Oln
OTaylor
#TAYLOR_2
G0 K0 L0 M0 O1 R0 U0 V0 
OMaclaurin
#TBSP_1
G0 K0 L0 M0 O0 R0 U0 V1 
Vtotally_bounded
#TDGROUP
G0 K0 L0 M3 O2 R1 U0 V2 
VTwo_Divisible
MTwo_Divisible_Group
MUniquely_Two_Divisible_Group
OCONGRD
OAV
R==>
VAffVect-like
MAffVect
#TDLAT_1
G0 K0 L0 M0 O18 R0 U0 V0 
ODomains_of
ODomains_Union
OD-Union
ODomains_Meet
OD-Meet
ODomains_Lattice
OClosed_Domains_of
OClosed_Domains_Union
OCLD-Union
OClosed_Domains_Meet
OCLD-Meet
OClosed_Domains_Lattice
OOpen_Domains_of
OOpen_Domains_Union
OOPD-Union
OOpen_Domains_Meet
OOPD-Meet
OOpen_Domains_Lattice
#TDLAT_2
G0 K0 L0 M0 O0 R0 U0 V3 
Vdomains-family
Vclosed-domains-family
Vopen-domains-family
#TDLAT_3
G0 K0 L0 M0 O0 R0 U0 V4 
Vanti-discrete
Valmost_discrete
Vextremally_disconnected
Vhereditarily_extremally_disconnected
#TERMORD
G0 K0 L0 M0 O3 R0 U0 V0 
OHT
OHM
ORed
#TEX_1
G0 K0 L0 M0 O3 R0 U0 V0 
Ocobool
OADTS
OSTS
#TEX_2
G0 K0 L0 M0 O1 R0 U0 V1 
OSspace
Vmaximal_discrete
#TEX_4
G0 K0 L0 M0 O3 R0 U0 V2 
Vanti-discrete-set-family
OMaxADSF
Vmaximal_anti-discrete
OMaxADSet
OMaxADSspace
#TIETZE
G0 K0 L0 M0 O0 R1 U0 V0 
Ris_absolutely_bounded_by
#TMAP_1
G0 K0 L0 M0 O3 R2 U0 V0 
Ris_continuous_at
Ris_not_continuous_at
O-extension_of_the_topology_of
Omodified_with_respect_to
Omodid
#TOLER_1
G0 K0 L0 M2 O4 R0 U0 V1 
OTotal
MTolSet
VTolClass-like
MTolClass
Oneighbourhood
OTolSets
OTolClasses
#TOPALG_1
G0 K0 L0 M0 O6 R0 U0 V0 
OPaths
OLoops
OFundamentalGroup
Opi_1
Opi_1-iso
ORealHomotopy
#TOPALG_2
G0 K0 L0 M0 O2 R0 U0 V0 
OConvexHomotopy
OR1Homotopy
#TOPALG_3
G0 K0 L0 M0 O1 R0 U0 V0 
OFundGrIso
#TOPALG_4
G0 K0 L0 M0 O2 R0 U0 V0 
OGr2Iso
OFGPrIso
#TOPALG_5
G0 K0 L0 M0 O5 R0 U0 V0 
OExtendInt
OPrj1
OPrj2
OcLoop
OCiso
#TOPDIM_1
G0 K0 L0 M0 O2 R0 U0 V2 
OSeq_of_ind
Vwith_finite_small_inductive_dimension
Vfinite-ind
Oind
#TOPGEN_1
G0 K0 L0 M0 O2 R2 U0 V4 
Ris_an_accumulation_point_of
ODer
Ris_isolated_in
Vdense-in-itself
Vperfect
Vscattered
Odensity
Vseparable
#TOPGEN_2
G0 K0 L0 M1 O2 R0 U0 V2 
OChi
MNeighborhood_System
Vfinite-weight
Vinfinite-weight
ODiscrWithInfin
#TOPGEN_3
G0 K0 L0 M0 O6 R1 U0 V1 
Vpoint-filtered
OSorgenfrey-line
Ris_local_minimum_of
Ocontinuum
O-powers
OClFinTop
O-PointClTop
O-DiscreteTop
#TOPGEN_4
G0 K0 L0 M0 O2 R1 U0 V8 
OTotFam
Vall-open-containing
Vall-closed-containing
Vclosed_for_countable_unions
Vclosed_for_countable_meets
VF_sigma
VG_delta
VT_1/2
Ris_a_condensation_point_of
OBorelSets
VBorel
#TOPGEN_5
G0 K0 L0 M0 O3 R0 U0 V1 
Oy=0-line
Oy>=0-plane
ONiemytzki-plane
VTychonoff
#TOPGRP_1
G1 K0 L0 M3 O1 R0 U0 V2 
MHomeomorphism
OHomeoGroup
GTopGrStr
VUnContinuous
VBinContinuous
MTopGroup
MTopologicalGroup
#TOPMETR
G0 K0 L0 M0 O3 R0 U0 V1 
OClosed-Interval-MSpace
Vbeing_ball-family
OR^1
OClosed-Interval-TSpace
#TOPREAL1
G0 K0 L0 M0 O6 R1 U0 V5 
Ris_an_arc_of
OR^2-unit_square
OL~
Vspecial
Vunfolded
Vs.n.c.
Vbeing_S-Seq
Vbeing_S-P_arc
Onorth_halfline
Oeast_halfline
Osouth_halfline
Owest_halfline
#TOPREAL2
G0 K0 L0 M1 O0 R0 U0 V1 
Vbeing_simple_closed_curve
MSimple_closed_curve
#TOPREAL4
G0 K0 L0 M0 O0 R1 U0 V2 
Ris_S-P_arc_joining
Vbeing_special_polygon
Vbeing_Region
#TOPREAL7
G0 K0 L0 M0 O1 R0 U0 V0 
Omax-Prod2
#TOPREALA
G0 K0 L0 M0 O2 R0 U0 V0 
OTrectangle
OR2Homeomorphism
#TOPREALB
G0 K0 L0 M0 O9 R0 U0 V0 
OIntIntervals
OTcircle
OTunit_circle
Oc[10]
Oc[-10]
OTopen_unit_circle
OCircleMap
OCircle2IntervalR
OCircle2IntervalL
#TOPS_1
G0 K0 L0 M0 O2 R0 U0 V6 
OInt 128
OFr 128
Vdense
Vboundary
Vnowhere_dense
Vcondensed
Vclosed_condensed
Vopen_condensed
#TOPS_2
G0 K0 L0 M0 O0 R0 U0 V1 
Vbeing_homeomorphism
#TOPS_3
G0 K0 L0 M0 O0 R0 U0 V1 
Veverywhere_dense
#TRANSGEO
G0 K0 L0 M1 O0 R3 U0 V6 
Ris_FormalIz_of
Ris_automorphism_of
Ris_DIL_of
VCongrSpace-like
MCongrSpace
Vpositive_dilatation
Vnegative_dilatation
Vdilatation
Vtranslation
Vcollineation
#TREAL_1
G0 K0 L0 M0 O2 R0 U0 V0 
OL[01] 180
OP[01] 180
#TREES_1
G0 K0 L0 M4 O6 R2 U0 V2 
Ris_a_prefix_of
Ris_a_proper_prefix_of
OProperPrefixes 128
VTree-like
MTree
Oelementary_tree 128
OLeaves
MLeaf
MSubtree
Owith-replacement
VAntiChain_of_Prefixes-like
MAntiChain_of_Prefixes
Oheight 128
Owidth 128
#TREES_2
G0 K0 L0 M4 O2 R0 U0 V3 
Vfinite-order
MChain
MLevel
O-level
VBranch-like
MBranch
VDecoratedTree-like
MDecoratedTree
Obranchdeg
#TREES_3
G0 K0 L0 M2 O3 R0 U0 V6 
OTrees
OFinTrees
Vconstituted-Trees
Vconstituted-FinTrees
Vconstituted-DTrees
MDTree-set
VTree-yielding
VFinTree-yielding
VDTree-yielding
MT-Substitution
Oroots
#TREES_4
G0 K0 L0 M1 O3 R0 U0 V0 
MNode
Oroot-tree
O-flat_tree
O-tree
#TREES_9
G0 K0 L0 M0 O4 R0 U0 V2 
Vroot
Vfinite-branching
OSubtrees
OFixedSubtrees
O-Subtrees
O-ImmediateSubtrees
#TREES_A
G0 K0 L0 M0 O1 R0 U0 V0 
Otree
#TRIANG_1
G1 K0 L0 M3 O5 R0 U2 V1 
Osymplexes
Vlower_non-empty
OFuncsSeq
ONatEmbSeq
Mtriangulation
GTriangStr
USkeletonSeq
UFacesAssign
MSymplex
MFace
Oface
OTriang
#TSEP_1
G0 K0 L0 M0 O0 R3 U0 V0 
Rare_not_separated
Rare_weakly_separated
Rare_not_weakly_separated
#TSEP_2
G0 K0 L0 M0 O0 R2 U0 V0 
Rconstitute_a_decomposition
Rdo_not_constitute_a_decomposition
#TSP_1
G0 K0 L0 M4 O0 R0 U0 V0 
MKolmogorov_space
Mnon-Kolmogorov_space
MKolmogorov_subspace
Mnon-Kolmogorov_subspace
#TSP_2
G0 K0 L0 M1 O1 R0 U0 V1 
Vmaximal_T_0
Mmaximal_Kolmogorov_subspace
OStone-retraction
#TURING_1
G1 K0 L0 M4 O24 R3 U2 V1 
OSegM
OPrefix
GTuringStr
USymbols
UAcceptS
MTape
OTape-Chg
MAll-State
MTran-Source
MTran-Goal
Ooffset
OHead
OTRAN
VAccept-Halt
OSum_Tran
Ris_1_between
RstoreData
OSumTuring
Rcomputes
OSucc_Tran
OSuccTuring
OZero_Tran
OZeroTuring
OU3(n)Tran
OU3(n)Turing
OUnionSt
OFirstTuringTran
OSecondTuringTran
OFirstTuringState
OSecondTuringState
OFirstTuringSymbol
OSecondTuringSymbol
OUniontran
OUnionTran
O';'
#TWOSCOMP
G0 K0 L0 M0 O39 R0 U0 V0 
Oand2
Oand2a
Oand2b
Onand2
Onand2a
Onand2b
Oor2
Oor2a
Oor2b
Onor2
Onor2a
Onor2b
Oxor2
Oxor2a
Oxor2b
Oand3
Oand3a
Oand3b
Oand3c
Onand3
Onand3a
Onand3b
Onand3c
Oor3a
Oor3b
Oor3c
Onor3
Onor3a
Onor3b
Onor3c
Oxor3
OCompStr
OCompCirc
OCompOutput
OIncrementStr
OIncrementCirc
OIncrementOutput
OBitCompStr
OBitCompCirc
#T_0TOPSP
G0 K0 L0 M1 O4 R1 U0 V0 
Rare_homeomorphic
OIndiscernibility
OIndiscernible
OT_0-reflex
OT_0-canonical_map
MT_0-TopSpace
#T_1TOPSP
G0 K0 L0 M0 O3 R0 U0 V0 
OClosed_Partitions
OT_1-reflex
OT_1-reflect
#UNIALG_1
G1 K0 L0 M2 O2 R0 U1 V1 
Vhomogeneous
MPFuncFinSequence
GUAStr
Ucharact
MUniversal_Algebra
Oarity 128
Osignature
#UNIALG_2
G0 K0 L0 M3 O9 R1 U0 V2 
MPFuncsDomHQN
OOperations
Moperation
Ris_closed_on
Vopers_closed
OOpers 128
MSubAlgebra
OUniAlgSetClosed
OConstants
Vwith_const_op
OGenUnivAlg
OSub
OUniAlg_join
OUniAlg_meet
OUnSubAlLattice
#UNIALG_3
G0 K0 L0 M1 O0 R0 U0 V0 
MSubAlgebra-Family
#UNIROOTS
G0 K0 L0 M0 O5 R0 U0 V0 
OMultGroup
O-roots_of_1
O-th_roots_of_1
Ounital_poly
Ocyclotomic_poly
#UPROOTS
G0 K0 L0 M1 O8 R0 U0 V0 
OcanFS
O-bag
MRbag
Opoly_shift
Opoly_quotient
Omultiplicity
OBRoots
Ofpoly_mult_root
Opoly_with_roots
#URYSOHN1
G0 K0 L0 M2 O4 R0 U0 V0 
Odyadic
ODYADIC
Odyad
Oaxis
MNbhd
MBetween
#URYSOHN3
G0 K0 L0 M2 O4 R0 U0 V0 
MDrizzle
MRain
Oinf_number_dyadic
OTempest
ORainbow
OThunder
#VALUAT_1
G0 K0 L0 M1 O3 R0 U0 V0 
OValuations_in
OFOR_ALL
Minterpretation
OValid
#VALUED_0
G0 K0 L0 M1 O0 R0 U0 V11 
Vcomplex-valued
Vext-real-valued
Vreal-valued
Vrational-valued
Vinteger-valued
Vnatural-valued
Vnon-zero
Vdecreasing
Vnon-decreasing
Vnon-increasing
Msubsequence
Vzeroed
#VALUED_1
G0 K0 L0 M0 O3 R0 U0 V0 
O(#)
O/"
OShift
#VALUED_2
G0 K0 L0 M0 O26 R0 U0 V12 
ODOMS
Vcomplex-functions-membered
Vext-real-functions-membered
Vreal-functions-membered
Vrational-functions-membered
Vinteger-functions-membered
Vnatural-functions-membered
OC_PFuncs
OC_Funcs
OE_PFuncs
OE_Funcs
OR_PFuncs
OR_Funcs
OQ_PFuncs
OQ_Funcs
OI_PFuncs
OI_Funcs
ON_PFuncs
ON_Funcs
Vcomplex-functions-valued
Vext-real-functions-valued
Vreal-functions-valued
Vrational-functions-valued
Vinteger-functions-valued
Vnatural-functions-valued
O(/)
O<->
O(-) 32
O</> 128
O[+]
O[-]
O[/] 128
O<+>
O<#> 128
O<++>
O<-->
O<##> 128
O<//> 128
#VECTMETR
G1 K0 L0 M2 O5 R0 U0 V3 
Vinternal
MGeometry
Visometric
OISOM
GRLSMetrStruct
Vtranslatible
ONorm
MRealLinearMetrSpace
ORLMSpace
OIsomGroup
OSubIsomGroupRel
#VECTSP10
G0 K0 L0 M0 O10 R0 U0 V0 
OStructVectSp
OCosetSet
OaddCoset
OzeroCoset
OlmultCoset
OVectQuot
OcoeffFunctional
Oker
OQFunctional
OCQFunctional
#VECTSP11
G0 K0 L0 M2 O1 R0 U0 V1 
Vwith_eigenvalues
Meigenvalue
Meigenvector
OUnionKers
#VECTSP_1
G1 K0 L0 M6 O3 R0 U1 V7 
OG_Real
MAddGroup
MAbGroup
Vright-distributive
Vleft-distributive
Vright_unital
OF_Real
Vwell-unital
Vleft_unital
MField
GVectSpStr
Ulmult
MScalar
MVector
Ocomp
VVectSp-like
MVectSp
VFanoian
#VECTSP_2
G2 K0 L0 M6 O4 R0 U1 V3 
McomRing
VdomRing-like
MdomRing
MSkew-Field
GRightModStr
Urmult
GBiModStr
OAbGr
OLeftModule
ORightModule
OBiModule
MLeftMod
VRightMod-like
MRightMod
VBiMod-like
MBiMod
#VECTSP_8
G0 K0 L0 M3 O1 R0 U0 V0 
MSubVS-Family
OFuncLatt
MSemilattice-Homomorphism
Msup-Semilattice-Homomorphism
#VFUNCT_1
G0 K0 L0 M0 O0 R1 U0 V0 
Ris_bounded_on
#WAYBEL10
G0 K0 L0 M1 O6 R0 U0 V0 
OClOpers
MSystem
OClosureSystems
OClImageMap
Oclosure_op
ODsupClOpers
OSubalgebras
#WAYBEL11
G0 K0 L0 M0 O2 R1 U0 V5 
Vinaccessible_by_directed_joins
Vclosed_under_directed_sups
Vproperty(S)
Vdirectly_closed
VScott
Ris_S-limit_of
OScott-Convergence
ONet-Str
#WAYBEL14
G0 K0 L0 M0 O0 R0 U0 V1 
Vjointly_Scott-continuous
#WAYBEL15
G0 K0 L0 M0 O1 R0 U0 V1 
Vatom
OATOM
#WAYBEL16
G0 K0 L0 M1 O1 R1 U0 V1 
MCLHomomorphism
Ris_FG_set
Vcompletely-irreducible
OIrr
#WAYBEL17
G0 K0 L0 M0 O2 R0 U0 V0 
O,...
OSCMaps
#WAYBEL18
G0 K0 L0 M0 O2 R1 U0 V1 
VTopSpace-yielding
Oproduct_prebasis
Ris_Retract_of
OSierpinski_Space
#WAYBEL19
G0 K0 L0 M1 O0 R0 U0 V1 
MTopPoset
VLawson
#WAYBEL20
G0 K0 L0 M0 O3 R0 U0 V1 
OEqRel
VCLCongruence
Okernel_op
Okernel_congruence
#WAYBEL21
G0 K0 L0 M2 O0 R0 U0 V1 
MSemilatticeHomomorphism
MEmbedding
Vlim_infs-preserving
#WAYBEL22
G0 K0 L0 M0 O2 R1 U0 V0 
Ris_FreeGen_set_of
OFixedUltraFilters
O-extension_to_hom
#WAYBEL23
G0 K0 L0 M1 O4 R0 U0 V5 
Vinfs-closed
Vsups-closed
Oweight
Vsecond-countable
MCLbasis
Vwith_bottom
Vwith_top
OsupMap
OidsMap
ObaseMap
#WAYBEL24
G0 K0 L0 M0 O1 R0 U0 V0 
OContMaps
#WAYBEL25
G0 K0 L0 M0 O1 R0 U0 V1 
OOmega
Vmonotone-convergence
#WAYBEL26
G0 K0 L0 M0 O4 R0 U0 V0 
O-POS_prod
O-TOP_prod
OoContMaps
O*graph
#WAYBEL27
G0 K0 L0 M0 O1 R0 U0 V3 
Vuncurrying
Vcurrying
Vcommuting
OUPS
#WAYBEL28
G0 K0 L0 M0 O2 R0 U0 V1 
Vgreater_or_equal_to_id
Olim_inf-Convergence
Oxi
#WAYBEL29
G0 K0 L0 M0 O2 R0 U0 V0 
OSigma
OTheta
#WAYBEL30
G0 K0 L0 M0 O1 R0 U0 V3 
O^0
Vwith_small_semilattices
Vwith_compact_semilattices
Vwith_open_semilattices
#WAYBEL31
G0 K0 L0 M0 O2 R0 U0 V0 
OCLweight
OWay_Up
#WAYBEL32
G0 K0 L0 M0 O1 R0 U0 V1 
Vorder_consistent
Oinf_net
#WAYBEL33
G0 K0 L0 M0 O1 R0 U0 V1 
Vlim-inf
OXi
#WAYBEL34
G0 K0 L0 M0 O8 R0 U0 V7 
OLowerAdj
OUpperAdj
O-INF_category
O-SUP_category
Vwaybelow-preserving
Vrelatively_open
O-INF(SC)_category
O-SUP(SO)_category
O-CL_category
O-CL-opp_category
Vcompact-preserving
Vfinite-sups-preserving
Vbottom-preserving
Vfinite-sups-inheriting
Vbottom-inheriting
#WAYBEL35
G0 K0 L0 M1 O4 R2 U0 V3 
Vextra-order
O-LowerMap
Mstrict_chain
OStrict_Chains
Ris_inductive_wrt
Rsatisfies_SIC_on
Vsatisfying_SIC
OSetBelow
Vsup-closed
OSupBelow
#WAYBEL_0
G1 K0 L0 M5 O9 R4 U1 V17 
Vdirected
Vfiltered
Vfiltered-infs-inheriting
Vdirected-sups-inheriting
Vantitone
GNetStr
Umapping
Mprenet
Mnet
Onetmap
Ris_eventually_in
Ris_often_in
Veventually-directed
Veventually-filtered
Odownarrow
Ouparrow
Vlower
Vupper
OIds
OFilt
OIds_0
OFilt_0
Ofinsups
Ofininfs
MSemilattice
Msup-Semilattice
MLATTICE
Rpreserves_inf_of
Rpreserves_sup_of
Vinfs-preserving
Vsups-preserving
Vmeet-preserving
Vjoin-preserving
Vfiltered-infs-preserving
Vdirected-sups-preserving
Vup-complete
V/\-complete
#WAYBEL_1
G0 K0 L0 M1 O2 R6 U0 V6 
Rex_min_of
Rex_max_of
Rhas_the_min_in
Rhas_the_max_in
Ris_minimum_of
Ris_maximum_of
MConnection
VGalois
Vupper_adjoint
Vlower_adjoint
Vprojection
Vclosure
Vkernel
Ocorestr
Oinclusion
#WAYBEL_2
G0 K0 L0 M0 O3 R0 U0 V2 
OFinSups
Oinf_op
Osup_op
Vsatisfying_MC
Vmeet-continuous
#WAYBEL_3
G0 K0 L0 M0 O2 R3 U0 V5 
Ris_way_below
R<<
R>>
Visolated_from_below
Owaybelow
Owayabove
Vsatisfying_axiom_of_approximation
Vnon-Empty
Vreflexive-yielding
Vlocally-compact
#WAYBEL_4
G0 K0 L0 M0 O11 R3 U0 V8 
O-waybelow
OIntRel
Vauxiliary(i)
Vauxiliary(ii)
Vauxiliary(iii)
Vauxiliary(iv)
Vauxiliary
OAux
OAuxBottom
O-below
O-above
OMonSet
ORel2Map
OMap2Rel
ODownMap
Vapproximating
OApp
Vsatisfying_SI
Vsatisfying_INT
Ris_directed_wrt
Ris_maximal_wrt
Ris_minimal_wrt
#WAYBEL_5
G0 K0 L0 M2 O4 R0 U0 V1 
MDoubleIndexedSet
O\//
O/\\
OSups
OInfs
Vcompletely-distributive
MCLSubFrame
#WAYBEL_6
G0 K0 L0 M0 O2 R0 U0 V5 
VOpen
Vmeet-irreducible
Vjoin-irreducible
OIRR
Vorder-generating
OPRIME
Vco-prime
#WAYBEL_7
G0 K0 L0 M0 O0 R2 U0 V1 
Ris_a_cluster_point_of
Ris_a_convergence_point_of
Vpseudoprime
#WAYBEL_8
G0 K0 L0 M0 O2 R0 U0 V3 
OCompactSublatt
Ocompactbelow
Vsatisfying_axiom_K
Valgebraic
Varithmetic
#WAYBEL_9
G1 K0 L0 M1 O2 R0 U0 V0 
O+id
Oopp+id
GTopRelStr
MTopLattice
#WEDDWITT
G0 K0 L0 M0 O5 R0 U0 V0 
OCentralizer
O-con_map
Oconjugate_Classes
Ocentralizer
OVectSp_over_center
#WEIERSTR
G0 K0 L0 M0 O6 R0 U0 V0 
Odist_max
Odist_min
Omin_dist_min
Omax_dist_min
Omin_dist_max
Omax_dist_max
#WELLFND1
G0 K0 L0 M0 O1 R1 U0 V1 
Owell_founded-Part
Ris_recursively_expressed_by
Vdescending
#WELLORD1
G0 K0 L0 M0 O3 R4 U0 V2 
O-Seg 128
Vwell_founded
Ris_well_founded_in
Vwell-ordering
Rwell_orders
O|_2 100
Ris_isomorphism_of
Rare_isomorphic
Ocanonical_isomorphism_of 100
#WELLORD2
G0 K0 L0 M0 O2 R1 U0 V0 
ORelIncl 128
Oorder_type_of 32
Ris_order_type_of
#XBOOLEAN
G0 K0 L0 M0 O11 R0 U0 V1 
OFALSE
OTRUE
Vboolean
O'not' 82
O'&' 80
O'or' 70
O=> 69
O<=> 69
O'nand'
O'nor'
O'xor'
O'\'
#XBOOLE_0
G0 K0 L0 M0 O5 R4 U0 V1 
Vempty
O{} 128
O\/ 32
O/\
O\ 32
O\+\ 30
Rmisses
Rc<
Rare_c=-comparable
Rmeets
#XCMPLX_0
G0 K0 L0 M0 O1 R0 U0 V2 
O<i>
Vcomplex
Vzero
#XREAL_0
G0 K0 L0 M0 O0 R0 U0 V1 
Vreal
#XXREAL_0
G0 K0 L0 M0 O5 R3 U0 V3 
Vext-real
O+infty 200
O-infty 200
R<=
R>=
R>
Vpositive
Vnegative
Omin 128
Omax 128
OIFGT
#XXREAL_1
G0 K2 L2 M0 O0 R0 U0 V0 
K[.
L.]
L.[
K].
#XXREAL_2
G0 K0 L0 M2 O0 R0 U0 V5 
MUpperBound
MLowerBound
Vleft_end
Vright_end
Vbounded_below
Vbounded_above
Vbounded
#YELLOW11
G0 K1 L1 M0 O2 R0 U0 V0 
ON_5
OM_3
K[#
L#]
#YELLOW13
G0 K0 L0 M1 O0 R0 U0 V1 
Mbasis
Vtopological_semilattice
#YELLOW15
G0 K0 L0 M0 O2 R0 U0 V1 
OMergeSequence
OComponents
Vin_general_position
#YELLOW16
G0 K0 L0 M0 O0 R5 U0 V1 
Ris_a_retraction_of
Ris_an_UPS_retraction_of
Ris_an_UPS_retract_of
VPoset-yielding
Rinherits_sup_of
Rinherits_inf_of
#YELLOW18
G0 K0 L0 M0 O5 R2 U0 V3 
Rare_opposite
Odualizing-func
Rare_dual
Vpara-functional
O-carrier_of
Othe_carrier_of
Vset-id-inheriting
Vconcrete
OConcretized
OConcretization
#YELLOW19
G0 K0 L0 M0 O3 R0 U0 V0 
ONeighborhoodSystem
Oa_filter
Oa_net
#YELLOW20
G0 K0 L0 M0 O0 R3 U0 V0 
Rhave_the_same_composition
Rare_isomorphic_under
Rare_anti-isomorphic_under
#YELLOW21
G0 K0 L0 M0 O5 R0 U0 V4 
Oas_1-sorted 255
OPOSETS
Vcarrier-underlaid
Vlattice-wise
Vwith_complete_lattices
Vwith_all_isomorphisms
O-UPS_category
O-CONT_category
O-ALG_category
#YELLOW_0
G0 K0 L0 M1 O1 R2 U0 V4 
Rex_sup_of
Rex_inf_of
MSubRelStr
Osubrelstr
Vmeet-inheriting
Vjoin-inheriting
Vinfs-inheriting
Vsups-inheriting
#YELLOW_1
G0 K0 L0 M0 O3 R0 U0 V1 
OInclPoset
OBoolePoset
VRelStr-yielding
OMonMaps
#YELLOW_2
G0 K0 L0 M0 O6 R0 U0 V0 
OSupMap
OIdsMap
O\\/
O//\
OSup
OInf
#YELLOW_3
G0 K1 L1 M0 O0 R0 U0 V0 
K["
L"]
#YELLOW_6
G0 K0 L0 M4 O7 R0 U0 V6 
Othe_universe_of
Vyielding_non-empty_carriers
OConstantNet
MSubNetStr
Msubnet
ONetUniv
Mnet_set
OIterated
OOpenNeighborhoods
MConvergence-Class
OConvergence
V(CONSTANTS)
V(SUBNETS)
V(DIVERGENCE)
V(ITERATED_LIMITS)
OConvergenceSpace
Vtopological
#YELLOW_7
G0 K0 L0 M0 O1 R0 U0 V0 
OComplMap
#YELLOW_8
G0 K0 L0 M0 O1 R1 U0 V4 
V-quasi_basis
VBaire
Virreducible
Ris_dense_point_of
Vsober
OCofinTop
#YELLOW_9
G0 K0 L0 M3 O0 R0 U0 V0 
MTopAugmentation
MTopExtension
MRefinement
#YONEDA_1
G0 K1 L1 M0 O2 R0 U0 V0 
OEnsHom
K<|
L,?>
OYoneda
#ZFMISC_1
G0 K1 L1 M0 O1 R1 U0 V1 
Obool 128
K[:
L:]
Rare_mutually_different
Vtrivial
#ZFMODEL1
G0 K0 L0 M0 O2 R2 U0 V0 
Odef_func'
Odef_func
Ris_definable_in
Ris_parametrically_definable_in
#ZFREFLE1
G0 K0 L0 M0 O1 R2 U0 V0 
R<==>
Ris_elementary_subsystem_of
OZF-axioms 200
#ZF_COLLA
G0 K0 L0 M0 O1 R2 U0 V0 
OCollapse 128
Ris_epsilon-isomorphism_of
Rare_epsilon-isomorphic
#ZF_FUND1
G0 K0 L0 M0 O4 R0 U0 V8 
Odecode 128
Ox". 200
Ocode 128
ODiagram 128
Vclosed_wrt_A1
Vclosed_wrt_A2
Vclosed_wrt_A3
Vclosed_wrt_A4
Vclosed_wrt_A5
Vclosed_wrt_A6
Vclosed_wrt_A7
Vclosed_wrt_A1-A7
#ZF_FUND2
G0 K0 L0 M0 O1 R0 U0 V1 
OSection
Vpredicatively_closed
#ZF_LANG
G0 K0 L0 M2 O17 R3 U0 V9 
OVAR 128
MVariable
Ox. 200
O'=' 90
O'in' 90
OWFF 68
VZF-formula-like
MZF-formula
Vbeing_equality
Vbeing_membership
Vconjunctive
Vatomic
Vdisjunctive
Vconditional
Vbiconditional
Vexistential
OVar1 66
OVar2 66
Othe_argument_of 66
Othe_left_argument_of 66
Othe_right_argument_of 66
Obound_in 66
Othe_scope_of 66
Othe_antecedent_of 66
Othe_consequent_of 66
Othe_left_side_of 66
Othe_right_side_of 66
Ris_immediate_constituent_of
Ris_subformula_of
Ris_proper_subformula_of
OSubformulae 66
#ZF_LANG1
G0 K0 L0 M0 O1 R0 U0 V0 
Ovariables_in 68
#ZF_MODEL
G0 K0 L0 M0 O9 R1 U0 V1 
OFree 72
OVAL 72
OSt 72
R|=
Othe_axiom_of_extensionality 128
Othe_axiom_of_pairs 128
Othe_axiom_of_unions 128
Othe_axiom_of_infinity 128
Othe_axiom_of_power_sets 128
Othe_axiom_of_substitution_for 128
Vbeing_a_model_of_ZF
#ZF_REFLE
G0 K0 L0 M2 O0 R0 U0 V1 
MSubclass
VDOMAIN-yielding
MDOMAIN-Sequence
