#ABCMIZ_0 G3 K0 L0 M1 O6 R2 U4 V7 GAdjectiveStr GTA-structure GTAS-structure Madjective O@--> Onon- Oadjs Otypes Oradix Oast Ris_applicable_to Ris_properly_applicable_to Uadjectives Unon-op Uadj-map Usub-map VMizar-widening-like Vwithout_fixpoints Vconsistent Vadj-structured Vadjs-typed Vnon-absorbing Vsubjected #ABCMIZ_1 G0 K0 L0 M9 O26 R0 U0 V10 Mvariable Mquasi-loci MConstructorSignature Mquasi-term Mquasi-adjective Mquasi-type Mexpression Mvaluation Ovars OVarPoset OQuasiLoci Oa_Type Oan_Adj Oa_Term Onon_op OModes OAttrs OConstructors Okind_of Oloci_of Oindex_of OMSVars Ovarcl OMinConstrSign OMaxConstrSign OQuasiTerms OQuasiAdjs OQuasiTypes Othe_base_of Ovars-function ONon Oat 128 Oidval O-trm Vground Vcompound Vinitialized Vconstructor Vpure Vwith_an_operation_for_each_sort Vwith_missing_variables Mterm-transformation Vsubstitution Vrelevant Virrelevant #ABIAN G0 K0 L0 M0 O1 R2 U0 V2 Rhas_a_fixpoint Rhas_no_fixpoint Vcovering O=_ Vempty-membered #ABSVALUE G0 K0 L0 M0 O2 R0 U0 V0 Oabs 150 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 R0 U0 V1 Vbeing_plane #AFINSQ_1 G0 K0 L0 M1 O2 R0 U0 V0 MXFinSequence O<%> 254 O^omega #AFINSQ_2 G0 K0 L0 M0 O2 R2 U0 V0 OSubXFinS OSgm0 R #ALGSPEC1 G0 K0 L0 M2 O1 R1 U0 V0 O-indexing Mrng-retract Rform_a_replacement_in MExtension #ALGSTR_0 G3 K0 L0 M0 O8 R0 U2 V11 GmultMagma UmultF GaddMagma UaddF GaddLoopStr OTrivial-addMagma OTrivial-addLoopStr OTrivial-multMagma OTrivial-multLoopStr OTrivial-multLoopStr_0 Vleft_complementable Vleft_add-cancelable Vright_add-cancelable Vleft_mult-cancelable Vright_mult-cancelable Vmult-cancelable Vleft_invertible Vright_invertible OTrivial-RLSStruct OTrivial-doubleLoopStr OTrivial-CLSStruct Valmost_right_invertible Valmost_left_cancelable Valmost_right_cancelable #ALGSTR_1 G0 K0 L0 M5 O4 R0 U0 V10 OExtract OL_Trivial Vleft_zeroed Vadd-left-cancelable Vadd-right-cancelable Vadd-left-invertible Vadd-right-invertible VLoop-like MLoop OmultL_Trivial Vcancelable MmultLoop MmultGroup OmultEX_0 Valmost_invertible Valmost_cancelable VmultLoop_0-like MmultLoop_0 MmultGroup_0 #ALGSTR_2 G0 K0 L0 M6 O1 R0 U0 V1 OdoubleEX MdoubleLoop MleftQuasi-Field Vleft-distributive 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 MmultSubmagma MRelators Ocanon_image OClassOp Oequ_rel Oequ_kernel Ofree_magma Ofree_magmaF Ofree_magma_carrier Ofree_magma_mult Ofree_magma_seq OIFXFinSequence Olength Othe_mult_induced_by Othe_submagma_generated_by Rextends #ALG_1 G0 K0 L0 M1 O7 R2 U0 V0 Ris_homomorphism 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 O7 R0 U0 V6 Vjump-only ONIC OJUMP OSUCC VInsLoc-antisymmetric OSTC Olocnum ONextLoc Vreally-closed Vpara-closed OLastLoc Vhalt-ending Vunique-halt Mpre-Macro MIL-Subset #AMISTD_2 G0 K0 L0 M0 O5 R0 U0 V7 OPA Vproduct-like OAddressPart OAddressParts Vwith_explicit_jumps Vwithout_implicit_jumps Vwith-non-trivial-Instruction-Locations Vins-loc-free OStop VIC-good VExec-preserving OCutLastLoc #AMISTD_3 G0 K0 L0 M0 O5 R0 U0 V0 OTrivialInfiniteTree OExecTree OFirstLoc OLocNums OLocSeq #AMI_1 G2 K0 L0 M11 O12 R2 U6 V14 Vwith_non-empty_elements GAMI-Struct UInstruction-Counter UInstruction-Locations UInstruction-Codes UInstructions UObject-Kind UExecution OTrivial-AMI Vvoid MInstruction-Location MInstruction OIC OObjectKind MState OExec Vhalting Ohalt VIC-Ins-separated Vdata-oriented Vsteady-programmed Vdefinite Osproduct OCurInstr OFollowing OComputation Vrealistic OResult OFinPartSt MFinPartState Vautonomic Vprogrammable Mpre-program Rcomputes Rdoes_not_compute Vcomputable MProgram MInsType Vstandard-ins OInsCodes Vwith-ins MIL-FinSequence MIL-Function MIL-DecoratedTree Vstored-program MPartState GMemoryStr #AMI_2 G0 K0 L0 M1 O17 R0 U0 V0 OSCM-Halt OSCM-Data-Loc OSCM-Instr-Loc OSCM-Instr OSCM-OK MSCM-State OSCM-Chg Oaddress_1 Oaddress_2 Ojump_address Ocjump_address Ocond_address OIFGT ONext OSCM-Exec-Res OSCM-Exec OSCM-Memory OSCM+FSA-Memory #AMI_3 G0 K0 L0 M1 O12 R2 U0 V1 OSCM MData-Location O:= OAddTo OSubFrom OMultBy ODivide Ogoto O=0_goto O>0_goto OStart-At Vprogrammed Rstarts_at Rhalts_at Odl. Oil. #AMI_4 G0 K0 L0 M0 O2 R0 U0 V0 OEuclide-Algorithm OEuclide-Function #AMI_5 G0 K0 L0 M0 O3 R0 U0 V1 OInsCode OProgramPart ODataPart Vdata-only #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 O6 R3 U0 V1 Vnon-zero Ris_Prop_Vect Rare_Prop Rare_LinDep OProper_Vectors_of OProportionality_as_EqRel_of ODir OProjectivePoints OProjectiveCollinearity OProjectiveSpace #ANPROJ_2 G0 K0 L0 M2 O0 R5 U0 V4 Rare_Prop_Vect Rlie_on_a_triangle Rare_perspective Rlie_on_an_angle Rare_half_mutually_not_Prop Vup-3-dimensional VVebleian Vat_least_3rank MCollProjectiveSpace Vat_most-3-dimensional MCollProjectivePlane #AOFA_000 G0 K0 L0 M4 O12 R6 U0 V8 Rnin OGenerators Oorbit Vwith_empty-instruction Vwith_catenation Vwith_if-instruction Vwith_while-instruction MpreIfWhileAlgebra MIfWhileAlgebra MAlgorithm OEmptyIns O\; 16 Oif-then-else Oif-then Owhile Ofor-do OElementaryInstructions OECIW-signature VECIW-strict Riteration_terminates_for Oiteration-degree Vcomplying_with_empty-instruction Vcomplying_with_catenation Rcomplies_with_if_wrt Rcomplies_with_while_wrt MExecutionFunction OTerminatingPrograms Vabsolutely-terminating Ris_terminating_wrt Ris_invariant_wrt #AOFA_I00 G0 K0 L0 M6 O12 R2 U0 V0 OINT-ElemIns MEnumeration MDenumeration MINT-Exec MINT-Variable MINT-Expression MINT-Array Ris_assignment_wrt Rform_assignment_wrt O*= 32 O+= 32 O/= 32 O%= 32 Oeq 32 Ogeq 32 Oleq 32 Ogt 32 Olt 32 Ois_odd Ois_even #ARMSTRNG G1 K0 L0 M4 O13 R8 U2 V19 GDB-Rel UDomains URelationship MDependency MSubset-Relation MDependency-set ODependencies Rholds_in R>|> ODependency-str Ris_at_least_as_informative_as ODependencies-Order V(F1) V(F2) V(F3) V(F4) Vfull_family MFull-family OMaximal_wrt OMaximal_in R^|^ V(M1) V(M2) V(M3) Osaturated-subsets Oclosed_attribute_subset V(B1) V(B2) Odeps_encl_by Oenclosure_of Ris_generator-set_of Ris_/\-irreducible_in Ris_/\-reducible_in O/\-IRR Ocandidate-keys V(C1) Vwithout_proper_subsets V(C2) V(DC1) V(DC2) V(DC3) V(DC4) V(DC5) V(DC6) Ocharact_set ODependency-closure Ris_p_i_w_ncv_of #ARROW G0 K0 L0 M0 O2 R4 U0 V0 OLinOrders OLinPreorders R<_ R>_ R<=_ R>=_ #ARYTM G0 K0 L0 M1 O1 R0 U0 V1 Mnumber Vreal O0 #ARYTM_0 G0 K0 L0 M0 O1 R0 U0 V0 Oinv #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 O8 R3 U0 V0 Rare_relative_prime Rdivides Olcm 32 Ohcf 32 ORED ORAT+ Onumerator 150 Odenominator 150 O/ O*' 128 R<=' #ASYMPT_0 G0 K0 L0 M0 O4 R2 U0 V7 Vpositive 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 O9 R0 U0 V0 Oseq_a^ Oseq_logn Oseq_n^ Oseq_const Oseq_n! OProb28 Oseq_prob28 OPOWEROF2SET OStep1 #AUTALG_1 G0 K0 L0 M1 O7 R0 U0 V0 OUAAut OUAAutComp OUAAutGroup OMSFuncs MMSFunctionSet OMSAAut OMSAAutComp OMSAAutGroup #AUTGROUP G0 K0 L0 M0 O6 R0 U0 V0 OAut OAutComp OAutGroup OInnAut OInnAutGroup OConjugate #BAGORDER G0 K0 L0 M1 O8 R0 U0 V0 OFinOrd OPosetMax OPosetMin OFinOrd-Approx OFinPoset Ominclude OSeqShift OMinElement MTermOrder #BCIALG_1 G2 K0 L0 M2 O4 R6 U1 V15 GBCIStr GBCIStr_0 UInternalDiff Vbeing_B Ris_B Vbeing_C Ris_C Vbeing_I Ris_I Vbeing_K Ris_K Vbeing_BCI-4 Ris_BCI-4 Vbeing_BCK-5 Ris_BCK-5 OBCI-EXAMPLE 16 OBCK-part OAtomSet OBranchV Vgenerated_by_atom VBCI-algebra-like MBCI-algebra VBCK-algebra-like MBCK-algebra Vquasi-associative Valternative Vpositive-implicative Vweakly-positive-implicative Vweakly-implicative Vp-Semisimple #BCIALG_2 G0 K0 L0 M3 O6 R0 U0 V3 Vleast Vgreatest Vnilpotent ML-congruence MR-congruence MI-congruence OIConSet OConSet OLConSet ORConSet OzeroEqC OEqClaOp #BCIALG_3 G0 K0 L0 M1 O0 R0 U0 V10 Vbeing_minimal Vbeing_greatest Vbeing_positive VBCI-commutative VBCI-weakly-commutative MCommutative-Ideal Vbeing_Iseki Vinvolutory VIseki_extension 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 MBCI-homomorphism OHK OHKOp OzeroHK Visotonic Vfinite-period #BCIIDEAL G0 K0 L0 M4 O1 R0 U0 V0 Oinitial_section Mp-ideal Massociative-ideal Mimplicative-ideal Mpositive-implicative-ideal #BHSP_1 G1 K0 L0 M1 O0 R1 U1 V1 GUNITSTR Uscalar VRealUnitarySpace-like MRealUnitarySpace Rare_orthogonal #BHSP_3 G0 K0 L0 M0 O0 R2 U0 V3 VCauchy Ris_Cauchy_sequence Ris_compared_to Vcomplete VHilbert #BHSP_5 G0 K0 L0 M2 O5 R0 U0 V0 MOrthogonalFamily MOrthonormalFamily Osetop_SUM Osetop_xPre_PROD Osetop_xPROD Osetopfunc OFunc_Seq #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 ONulForm OFormFunctional OFunctionalFAF OFunctionalSAF Odiagker Oleftker Orightker OLKer OLQForm ORKer ORQForm OQForm VadditiveFAF VadditiveSAF VhomogeneousFAF VhomogeneousSAF Vdegenerated-on-left Vdegenerated-on-right MForm Mbilinear-Form #BINARITH G0 K0 L0 M0 O5 R1 U0 V0 O'xor' 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 #BINARI_5 G0 K0 L0 M0 O3 R0 U0 V0 O'nand' O'nor' O'xnor' #BINOM G0 K0 L0 M0 O2 R0 U0 V1 Vadd-cancelable 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 O11 R0 U0 V0 Oinvcomplex Odivcomplex Oinvreal Odivreal Ocomprat Oinvrat Oaddrat Odiffrat Omultrat Odivrat Odiffint #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 #BOOLE G0 K0 L0 M0 O5 R3 U0 V0 O{} 128 O\/ 32 O/\ O\ 32 Rmeets Rmisses O\+\ 30 Rc< #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 M3 O11 R3 U0 V2 Oproj 128 MMap 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_retraction Ris_a_retract_of Ris_an_SDR_of #BORSUK_2 G0 K0 L0 M0 O0 R1 U0 V1 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 V1 OIRRAT Vwith_proper_subsets #BORSUK_6 G0 K0 L0 M1 O10 R1 U0 V0 MHomotopy ORePar O1RP O2RP O3RP OIAA OIBB OICC OLowerLeftUnitTriangle OUpperUnitTriangle OLowerRightUnitTriangle Rare_connected #BROUWER G0 K0 L0 M0 O3 R0 U0 V0 OTdisk OBR-map ODiffElems #BSPACE G0 K0 L0 M1 O13 R0 U0 V1 Mchar-func Ochar-funcs Ochar-func-sum Ochar-func-zero Ochar-func-scalar-mult Ochar-func-space Osingleton-char-funcs VSingleton Osingleton-char-func OZ_2 Obspace-sum Obspace-scalar-mult Obspace Osingletons O\*\ #BVFUNC_1 G0 K0 L0 M0 O10 R1 U0 V0 O'imp' 15 O'eqv' 14 OBVF OPj OO_el 255 OI_el 255 OB_INF 255 OB_SUP 255 Ris_dependent_of OLift OGPart #BVFUNC_2 G0 K0 L0 M0 O1 R3 U0 V1 Ris_upper_min_depend_of Vindependent Ris_a_coordinate OCompF Ris_independent_of #C0SP1 G0 K0 L0 M1 O4 R0 U0 V5 OR_Algebra_of_BoundedFunctions OR_Normed_Algebra_of_BoundedFunctions Vmultiplicatively-closed Vadditively-closed Vadditively-linearly-closed Omult_ OOne_ Vscalar-mult-cancelable Vhaving-inverse MSubring #C0SP2 G0 K0 L0 M0 O4 R0 U0 V0 OContinuousFunctions OR_Algebra_of_ContinuousFunctions OR_Normed_Algebra_of_ContinuousFunctions OContinuousFunctionsNorm #CALCUL_1 G0 K0 L0 M0 O3 R4 U0 V1 OAnt OSuc Oset_of_CQC-WFF-seq Ris_tail_of Ris_a_correct_step Ris_formal_provable_from Ris_Subsequence_of Va_proof #CALCUL_2 G0 K0 L0 M0 O4 R0 U0 V0 OImpl OBegin OPer OIdFinS #CANTOR_1 G0 K0 L0 M2 O4 R0 U0 V2 OUniCl Mbasis OIntersect OFinMeetCl Mprebasis Othe_Cantor_set 200 Vquasi_basis Vquasi_prebasis #CARD_1 G0 K0 L0 M1 O4 R2 U0 V2 Vcardinal MCardinal R<=` R<` OCard 128 Onextcard 128 Vlimit_cardinal Oalef 128 Ocard 128 #CARD_2 G0 K0 L0 M0 O2 R0 U0 V0 O+` 32 O*` #CARD_3 G0 K0 L0 M1 O5 R0 U0 V1 VCardinal-yielding MCardinal-Function Odisjoin 128 Oproduct 128 Opi 128 OProduct 128 Oproduct" 128 #CARD_4 G0 K0 L0 M0 O0 R0 U0 V1 Vcountable #CARD_5 G0 K0 L0 M1 O2 R0 U0 V2 MAleph Ocf O-powerfunc_of Vregular Virregular #CARD_FIL G0 K0 L0 M1 O6 R9 U0 V4 Odual Ris_multiplicative_with Ris_additive_with Ris_complete_with Vuniform OExtend_Filter OFilters OFrechet_Filter OFrechet_Ideal RGCH Ris_inaccessible_cardinal Vstrong_limit Ris_strong_limit_cardinal Vstrongly_inaccessible Ris_strongly_inaccessible_cardinal Vmeasurable Ris_measurable_cardinal Opredecessor MInf_Matrix Ris_Ulam_Matrix_of #CARD_FIN G0 K0 L0 M0 O2 R0 U0 V1 OChoose OCard_Intersection Vfinite-yielding #CARD_LAR G0 K0 L0 M0 O2 R6 U0 V4 Ris_unbounded_in Ris_closed_in Ris_club_in Vunbounded OLBound Vstationary Ris_stationary_in Olimpoints VMahlo Ris_Mahlo Vstrongly_Mahlo Ris_strongly_Mahlo #CATALAN1 G0 K0 L0 M0 O1 R0 U0 V0 OCatalan #CATALAN2 G0 K0 L0 M1 O2 R0 U0 V1 ODomin_0 Vdominated_by_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 O6 R1 U6 V9 O.--> GCatStr UObjects UMorphisms UDom UCod UComp UId MObject MMorphism Ocod 128 OHom 128 VCategory-like MCategory O1Cat 255 Vmonic Vepi Vinvertible Vterminal Vinitial MFunctor OObj Visomorphic Ris_an_isomorphism 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 O4 R2 U0 V2 Ocods 128 O"*" Vretraction Vcoretraction Oterm 250 Oinit 250 MProjections_family Ris_a_product_wrt MInjections_family Ris_a_coproduct_wrt #CAT_4 G2 K1 L1 M2 O15 R0 U8 V4 O:-> 128 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 O[0] 250 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 #CFDIFF_1 G0 K0 L0 M2 O1 R0 U0 V0 MC_LINEAR MC_REST OInvShift #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 V2 Vnumber-like Vmultiple MGap MGrating Ocells MCell Oinfinite-cell Ostar Odel Rbounds MGrChain #CHORD G0 K0 L0 M3 O3 R1 U0 V5 Vminlength O.AdjacentSet MAdjGraph Vsimplicial Vchordal Vchordless Rare_adjacent MVertexSeparator Vminimal O.index MVertexScheme O.followSet #CIRCCMB3 G0 K0 L0 M0 O1 R0 U0 V5 Vone-gate Vstabilizing Vwith_stabilization-limit Vwith_nonpair_inputs Vwith_natural_inputs Ostabilization-time #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 O5 R0 U0 V1 OFix_inp OFix_inp_ext OIGTree OIGValue Vstable OInitialComp #CLASSES1 G0 K0 L0 M0 O4 R1 U0 V2 Vsubset-closed VTarski Ris_Tarski-Class_of OTarski-Class 200 ORank 200 Othe_transitive-closure_of 128 Othe_rank_of 200 #CLASSES2 G0 K0 L0 M3 O4 R0 U0 V0 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 O4 R0 U1 V1 MMSSetOp Vtopological GMSClosureStr UFamily OMSFull MMSClosureSystem MMSClosureOperator OMSFixPoints OClOp->ClSys OClSys->ClOp #CLOSURE2 G1 K0 L0 M4 O2 R2 U0 V0 Rin' Rc=' OBool MSubsetFamily MSetOp GClosureStr OFull MClosureSystem MClosureOperator #CLOSURE3 G0 K0 L0 M0 O3 R0 U0 V0 Osupp OMSUnion OSubAlgCl #CLVECT_1 G2 K0 L0 M2 O0 R0 U0 V2 GCLSStruct GCNORMSTR VComplexLinearSpace-like MComplexLinearSpace VComplexNormSpace-like MComplexNormSpace #COHSP_1 G0 K0 L0 M0 O8 R1 U0 V11 OFlatCoh OSub_of_Fin Vc=directed Vc=filtered Vmultiplicative 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 V1 MRelation3 GCollStr UCollinearity MCollSp Vproper #COMBGRAS G1 K0 L0 M1 O2 R0 U2 V5 Vclique VSTAR VTOP Vmaximal_clique Vincidence_preserving GIncProjMap Upoint-map Uline-map Oincprojmap MPartialLinearSpace OG_ #COMMACAT G0 K0 L0 M0 O8 R0 U0 V0 O`11 255 O`12 255 O`21 255 O`22 255 OcommaObjs OcommaMorphs OcommaComp Ocomma #COMPACT1 G0 K0 L0 M0 O1 R0 U0 V7 Vcompactification Vrelatively-compact Vpre-compact Vlocally-relatively-compact Vlocally-closed/compact Vliminally-relatively-compact Vliminally-compact OOne-Point_Compactification #COMPLEX1 G0 K2 L2 M0 O5 R0 U0 V0 OCOMPLEX 128 ORe 128 OIm 128 K[* L*] O0c 128 O1r 128 K|. L.| #COMPLEX2 G0 K0 L0 M0 O3 R0 U0 V0 OF_tize OC_tize Oangle #COMPLFLD G0 K0 L0 M0 O1 R0 U0 V0 OF_Complex #COMPLSP1 G0 K0 L0 M0 O7 R0 U0 V0 Oaddcomplex 128 Ocompcomplex 128 Odiffcomplex 128 Omultcomplex 128 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 O0 R0 U0 V6 Vcentered Vcompact VT_1 VT_2 VT_3 VT_4 #COMPUT_1 G0 K0 L0 M0 O13 R1 U0 V11 Vto-naturals Vfrom-natural-fseqs 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[^] O[pred] O[-] #COMSEQ_1 G0 K0 L0 M1 O0 R0 U0 V0 MComplex_Sequence #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 U4 V4 UAttributes 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 O2 R0 U0 V0 Ma_union_of_components ODown OUp #CONVEX1 G0 K0 L0 M0 O2 R0 U0 V0 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 Oepigraph OAdd_in_Prod_of_RLS OMult_in_Prod_of_RLS OProd_of_RLS ORLS_Real #CQC_LANG G0 K0 L0 M2 O3 R0 U0 V1 OIFEQ MSubstitution OSubst OCQC-WFF 254 VCQC-variable_list-like MCQC-variable_list #CQC_SIM1 G0 K0 L0 M0 O9 R2 U0 V0 ONEGATIVE OCON OUNIVERSAL OATOMIC OQuantNbr OSepFunc ONBI OSepVar Ris_Sep-closed_on OSepQuadruples 100 Rare_similar #CQC_THE1 G0 K0 L0 M0 O4 R3 U0 V2 Vbeing_a_theory Ris_a_theory OCn OProof_Step_Kinds Ris_a_correct_step_wrt Ris_a_proof_wrt OEffect OTAUT 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 OLinear_Space_of_ComplexSequences Othe_set_of_l2ComplexSequences Ocl_scalar GCUNITSTR OComplex_l2_Space VComplexUnitarySpace-like MComplexUnitarySpace OCZeroseq #CSSPACE3 G0 K0 L0 M0 O3 R0 U0 V0 Othe_set_of_l1ComplexSequences OComplex_l1_Space Ocl_norm #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 O15 R4 U0 V5 Ris_Dickson-basis_of Vquasi_ordered VDickson O<=E Omindex Omin-classes Ris_Minimal_wrt Ris_Minimal_in Ris_Well_founded_in VWell_founded Vweakly-ascending ODickson-bases O\~ ONATOrd OOrderedNAT Vadmissible ONaivelyOrderedBags OLexOrder OInvLexOrder OGraded OGrLexOrder OGrInvLexOrder OBlockOrder OTotDegree #DIFF_1 G0 K1 L1 M1 O9 R0 U0 V1 K[! L!] OfD Oforward_difference Ofdif ObD Obackward_difference Obdif OcD Ocentral_difference Ocdif VSequence-yielding MSeq_Sequence #DILWORTH G0 K0 L0 M4 O4 R0 U0 V5 MClique-partition Omaximals Ominimals MStableSet Vwith_finite_stability# Ostability# Vstrong-chain Vwith_finite_clique# Oclique# MColoring MClique VClique-wise VStableSet-wise #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 MdistProbFinS Ouniform_distribution Owhole_event Oevent_pick Ofrequency OFDprobability Odistribution_family OGenProbSEQ OFinseq-EQclass R-are_prob_equivalent OFDprobSEQ Odistribution OfreqSEQ OUniform_FDprobSEQ Ris_uniformly_distributed #DTCONSTR G0 K0 L0 M3 O14 R0 U0 V3 Oroots OTS OPeanoNat Vwith_terminals Vwith_nonterminals Vwith_useful_nonterminals MTerminal MNonTerminal MSubtreeSeq Oplus-one OPN-to-NAT OPNsucc ONAT-to-PN OFlattenSeq OTerminalString OPreTraversal OPostTraversal OTerminalLanguage OPreTraversalLanguage OPostTraversalLanguage #DYNKIN G0 K0 L0 M1 O5 R0 U0 V1 Ofollowed_by OseqIntersection Vintersection_stable Odisjointify MDynkin_System Ogenerated_Dynkin_System ODynSys #ENDALG G0 K0 L0 M0 O6 R0 U0 V1 OUAEnd OUAEndComp OUAEndMonoid OMSAEnd OMSAEndComp OMSAEndMonoid Vunity-preserving #ENS_1 G0 K0 L0 M0 O10 R1 U0 V1 OMaps 128 Oid$ Vsurjective Ris_a_surjection 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 OFinSeq_log OInfor_FinSeq_of OEntropy OEntropy_of_Cond_Prob OEntropy_of_Joint_Prob OMx2FinS #EQREL_1 G0 K0 L0 M2 O2 R0 U0 V1 Onabla VEquivalence_Relation-like MEquivalence_Relation OClass Ma_partition #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 Oplane_of_REAL Rare_coplane Odist_v #EUCLID_2 G0 K1 L1 M0 O0 R0 U0 V0 K|( L)| #EUCLID_3 G0 K0 L0 M0 O13 R2 U0 V0 Ocpx2euc Oeuc2cpx OTriangle Oinside_of_triangle Oclosed_inside_of_triangle Ooutside_of_triangle Rare_ldependent2 Rare_lindependent2 Otricord1 Otricord2 Otricord3 Otrcmap1 Otrcmap2 Otrcmap3 Oplane #EUCLID_4 G0 K0 L0 M0 O2 R0 U0 V0 ORn2Fin OTPn2Rn #EUCLID_5 G0 K1 L1 M0 O1 R0 U0 V0 K|{ L}| O #EUCLID_6 G0 K0 L0 M0 O2 R0 U0 V0 Othe_area_of_polygon3 Othe_perimeter_of_polygon3 #EUCLID_7 G0 K0 L0 M1 O6 R0 U0 V5 VR-orthogonal VR-orthonormal VR-normal Vlinear_manifold OL_Span OREAL-L OR2NS ORN_Base OProjFinSeq Oaccum MOrthogonal_Basis Vorthogonal_basis #EUCLID_8 G0 K0 L0 M0 O5 R0 U0 V0 OVFunc OVFuncdiff O O O #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 O23 R0 U2 V2 GG_Net Uentrance Uescape Oechaos 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_adjac Oe_circulation #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 R3 U0 V1 Ris_continuous_in Ris_continuous_on Ris_Lipschitzian_on VLipschitzian #FCONT_2 G0 K0 L0 M0 O0 R1 U0 V0 Ris_uniformly_continuous_on #FDIFF_1 G0 K0 L0 M2 O2 R2 U0 V3 Vconvergent_to_0 VREST-like MREST 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 O19 R0 U0 V0 Ochaos 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_adjac Of_circulation #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 R0 U0 V0 MFile #FILTER_0 G0 K1 L1 M2 O2 R2 U0 V3 MFilter K<. L.) Vbeing_ultrafilter Ris_ultrafilter Vprime 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 K2 L2 M2 O0 R1 U0 V0 MIdeal K(. L.> Ris_max-ideal K[# L#] MSublattice #FINSEQOP G0 K0 L0 M0 O1 R2 U0 V1 Ris_an_inverseOp_wrt Vhaving_an_inverseOp Rhas_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 O^ VFinSubsequence-like MFinSubsequence OSgm 128 OSeq 128 V-long VFinSequence-membered #FINSEQ_2 G0 K0 L0 M2 O3 R0 U0 V0 Oidseq 128 O|-> MFinSequenceSet MFinSequence-DOMAIN O-tuples_on 128 #FINSEQ_4 G0 K0 L0 M0 O4 R2 U0 V0 Ris_one-to-one_at Rjust_once_values O<- 100 O/. 100 O.. 100 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_7 G0 K0 L0 M0 O2 R0 U0 V0 OReplace OSwap #FINSEQ_8 G0 K0 L0 M0 O7 R6 U0 V0 Osmid Oovlpart Oovlcon Oovlldiff Oovlrdiff Rseparates_uniquely Ris_a_record_of Ris_substring_of Ris_preposition_of Ris_postposition_of Ris_terminated_by Oaddcr Oinstr #FINSET_1 G0 K0 L0 M0 O0 R0 U0 V2 Vfinite Vinfinite #FINSOP_1 G0 K0 L0 M0 O3 R0 U0 V0 O"**" 48 OfinSeg 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 OFinf OFdfl OFcl OFint Rare_mutually_symmetric #FINTOPO4 G0 K0 L0 M0 O4 R1 U0 V0 Ris_continuous OFTSC1 OFTSL1 ONbdc1 ONbdl1 #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 G1 K0 L0 M0 O13 R0 U1 V1 GFT_Space_Str UNbd OU_FT OFT{0} Vfilled O^delta O^deltai O^deltao O^i O^b O^s O^n O^f O^fb O^fi OSinglRel #FLANG_1 G0 K0 L0 M0 O1 R0 U0 V0 OLex 255 #FLANG_3 G0 K0 L0 M0 O1 R0 U0 V0 O|^.. #FRAENKEL G0 K0 L0 M1 O0 R0 U0 V1 Vfunctional MFUNCTION_DOMAIN #FRECHET G0 K0 L0 M0 O2 R1 U0 V3 Vfirst-countable Ris_convergent_to VFrechet Vsequential OREAL? OBalls #FRECHET2 G0 K0 L0 M1 O1 R0 U0 V0 Msubsequence OCl_Seq #FREEALG G0 K0 L0 M1 O12 R0 U0 V3 Vdisjoint_with_NAT Vwith_zero Vwithout_zero Ooper MGeneratorSet OREL ODTConUA OSym 255 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 M0 O12 R6 U3 V3 GFSM UTran UInitS 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 Vfinal 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 O-TwoStatesMooreSM Vcalculating_type GSM_Final UFinalS GMoore-SM_Final Ris_result_of Ris_accessible_via Rleads_to_final_state_of #FSM_3 G2 K0 L0 M1 O4 R0 U0 V0 Gsemiautomaton Gautomaton Mepsilon-automaton Oleft-Lang Oright-Lang Ochop O_bool #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 O3 R0 U0 V0 O--> 16 O[:] 80 O[;] 80 #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 V3 VFunction-like MFunction O. 100 Oid 128 Vone-to-one V-compatible #FUNCT_2 G0 K0 L0 M1 O1 R0 U0 V2 Vquasi_total OFuncs 128 VPermutation-like MPermutation #FUNCT_3 G0 K0 L0 M0 O5 R0 U0 V0 Ochi 128 Oincl 128 Opr1 128 Opr2 128 Odelta 128 #FUNCT_4 G0 K1 L1 M0 O3 R0 U0 V0 O+* K|: L:| Oiter O+~ #FUNCT_5 G0 K0 L0 M0 O6 R0 U0 V0 Oproj1 128 Oproj2 128 Ocurry 128 Ouncurry 128 Ocurry' 128 Ouncurry' 128 #FUNCT_6 G0 K0 L0 M0 O4 R0 U0 V0 OSubFuncs 128 Odoms 128 Orngs 128 OFrege #FUNCT_7 G0 K0 L0 M1 O5 R1 U0 V1 OIn Requal_outside Ocompose Oapply Ofirstdom Olastrng VFuncSeq-like MFuncSequence #FUNCT_8 G0 K0 L0 M0 O1 R2 U0 V3 Osignum Ris_even_on Ris_odd_on Vwith_symmetrical_domain Vquasi_even Vquasi_odd #FUNCT_9 G0 K0 L0 M0 O0 R0 U0 V2 Vperiodic V-periodic #FUZZY_1 G0 K0 L0 M4 O5 R0 U0 V0 MMembership_Func MFuzzySet O1_minus MEmpty_FuzzySet MUniversal_FuzzySet OEMF OUMF Oab_difMF Oab_dif #FUZZY_2 G0 K0 L0 M0 O1 R0 U0 V0 O++ 32 #FUZZY_3 G0 K0 L0 M4 O2 R0 U0 V0 MRMembership_Func MFuzzyRelation MZero_Relation MUniverse_Relation OZmf OUmf #FUZZY_4 G0 K0 L0 M0 O2 R0 U0 V0 Oconverse OImf #FVSUM_1 G0 K0 L0 M0 O2 R0 U0 V0 Omultfield Odiffield #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 OGFA0CarryStr OGFA0CarryICirc OGFA0CarryOutput OGFA0CarryCirc OGFA0AdderStr OGFA0AdderCirc OGFA0AdderOutput OBitGFA0Str OBitGFA0Circ OBitGFA0CarryOutput OBitGFA0AdderOutput OGFA1CarryIStr OGFA1CarryStr OGFA1CarryICirc OGFA1CarryOutput OGFA1CarryCirc OGFA1AdderStr OGFA1AdderCirc OGFA1AdderOutput OBitGFA1Str OBitGFA1Circ OBitGFA1CarryOutput OBitGFA1AdderOutput OGFA2CarryIStr OGFA2CarryStr OGFA2CarryICirc OGFA2CarryOutput OGFA2CarryCirc OGFA2AdderStr OGFA2AdderCirc OGFA2AdderOutput OBitGFA2Str OBitGFA2Circ OBitGFA2CarryOutput OBitGFA2AdderOutput OGFA3CarryIStr OGFA3CarryStr OGFA3CarryICirc OGFA3CarryOutput OGFA3CarryCirc 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 M8 O32 R6 U0 V8 OVertexSelector OEdgeSelector OSourceSelector OTargetSelector O_GraphSelectors Othe_Vertices_of Othe_Edges_of Othe_Source_of Othe_Target_of OcreateGraph O.adj 160 O.allNeighbors() 160 O.degree() 160 O.edgesBetween 160 O.edgesDBetween 160 O.edgesIn() 160 O.edgesInOut 160 O.edgesInOut() 160 O.edgesInto 160 O.edgesOut() 160 O.edgesOutOf 160 O.inDegree() 160 O.inNeighbors() 160 O.Lifespan() 160 O.order() 160 O.outDegree() 160 O.outNeighbors() 160 O.Result() 160 O.set 160 O.size() 160 O.strict O.-> MGraphStruct M_Graph MinducedSubgraph MremoveVertex MremoveVertices MremoveEdge MremoveEdges MGraphSeq RJoins RDJoins RSJoins RDSJoins R== R!= V[Graph-like] Vnon-Dmulti VDsimple Vloopless Vendvertex VGraph-yielding Vnon-trivial Vspanning #GLIB_001 G0 K0 L0 M8 O22 R3 U0 V3 MVertexSeq MEdgeSeq MWalk MTrail MDTrail MDWalk MDPath MSubwalk O.addEdge 160 O.append 160 O.cut 160 O.edges() 160 O.edgeSeq() 160 O.find 160 O.first() 160 O.last() 160 O.length() 160 O.remove 160 O.reverse() 160 O.rfind 160 O.vertexAt 160 O.vertexSeq() 160 O.vertices() 160 O.walkOf 160 O.allWalks() 160 O.allTrails() 160 O.allPaths() 160 O.allDWalks() 160 O.allDTrails() 160 O.allDPaths() 160 VTrail-like VCycle-like Vvertex-distinct Ris_Walk_from Ris_minlength_path_of Ris_minlength_dpath_of #GLIB_002 G0 K0 L0 M1 O4 R1 U0 V3 MComponentSet Vacyclic VComponent-like Vcut-vertex O.componentSet() 160 O.numComponents() 160 O.reachableFrom 160 O.reachableDFrom 160 Ris_DTree_rooted_at #GLIB_003 G0 K0 L0 M28 O21 R0 U0 V11 OWeightSelector OWeightVSelector OELabelSelector OELabelVSelector OVLabelSelector OVLabelVSelector Othe_Weight_of Othe_WeightV_of Othe_ELabel_of Othe_ELabelV_of Othe_VLabel_of Othe_VLabelV_of V[Weighted] V[ELabeled] V[VLabeled] MWGraph MEGraph MVGraph MWEGraph MWVGraph MEVGraph MWEVGraph MWGraphSeq MEGraphSeq MVGraphSeq MWEGraphSeq MWVGraphSeq MEVGraphSeq MWEVGraphSeq O.cost() 160 O.setWeight 160 O.setELabel 160 O.setVLabel 160 O.weightSeq() 160 O.labelEdge 160 O.labelVertex 160 O.labeledE() 160 O.labeledV() 160 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 #GLIB_004 G0 K0 L0 M5 O13 R2 U0 V1 MDIJK:Labeling MDIJK:LabelingSeq MPRIM:Labeling MPRIM:LabelingSeq Ris_mincost_DTree_rooted_at Ris_mincost_DPath_from MminimumSpanningTree Vmin-cost O.min_DPath_cost 160 ODIJK:NextBestEdges 160 ODIJK:Step 160 ODIJK:Init 160 ODIJK:CompSeq 160 ODIJK:SSSP 160 OPRIM:NextBestEdges 160 OPRIM:Init 160 OPRIM:Step 160 OPRIM:CompSeq 160 OPRIM:MST 160 O.allWSubgraphs() 160 OWGraphSelectors #GLIB_005 G0 K0 L0 M4 O12 R5 U0 V1 MFF:ELabeling MAP:VLabeling Ris_forward_edge_wrt Ris_backward_edge_wrt Ris_augmenting_wrt MAP:VLabelingSeq O.flow 160 O.flowSeq O.tolerance MFF:ELabelingSeq Rhas_valid_flow_from Vnatural-weighted Rhas_maximum_flow_from OAP:NextBestEdges 160 OAP:Step 160 OAP:CompSeq 160 OAP:FindAugPath 160 OAP:GetAugPath 160 OFF:CompSeq OFF:Step OFF:PushFlow 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 OExCl OEx-bound_in OEx-the_scope_of Vnegation_faithful Vwith_examples #GRAPHSP G0 K0 L0 M0 O12 R6 U0 V0 Owhile_do Orepeat Ofindmin OOuterVx OArgmin Onewpathcost ORelax RhasBetterPathAt ODijkstraAlgorithm Ris_Input_of_Dijkstra_Alg Ris_vertex_seq_at Ris_simple_vertex_seq_at OUnusedVx OUsedVx Ris_oriented_edge_seq_of OXEdge OWeight Requal_at #GRAPH_1 G1 K0 L0 M7 O5 R3 U4 V6 GMultiGraphStruct UVertices UEdges USource UTarget VGraph-like MGraph Ris_sum_of Voriented Vnon-multi Vsimple Rjoins Rare_incident VPath-like MPath MOrientedPath Vcyclic MCycle MOrientedCycle MSubgraph OVerticesCount OEdgesCount OEdgesIn OEdgesOut ODegree MEdge #GRAPH_2 G0 K0 L0 M0 O4 R3 U0 V2 O-cut O^' VTwoValued VAlternating O-VSet Ris_vertex_seq_of Ralternates_vertices_in Overtex-seq Ris_non_decreasing_on #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 Ris_weight_of Ris_weight>=0of Ris_orientedpath_of Ris_acyclicpath_of OOrientedPaths OAcyclicPaths OReal>=0 ORealSequence Ocost Ris_shortestpath_of RislongestInShortestpath Overtices #GRCAT_1 G1 K0 L0 M4 O11 R1 U1 V4 OTrivialGroup OMorphs Ocat Vadditive 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 #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 M0 O6 R2 U0 V3 Vunital VGroup-like O1. Oinverse_op 124 Opower 124 O|^ 90 Vbeing_of_order_0 Ris_not_of_order_0 Ris_of_order_0 Oord 128 OOrd 124 #GROUP_10 G0 K0 L0 M1 O10 R4 U0 V1 MLeftOperation Othe_extension_of_left_operation_of Othe_extension_of_left_translation_of Othe_fixed_points_of Othe_left_translation_of Othe_left_operation_of Othe_orbit_of Othe_orbits_of Othe_sylow_p-subgroups_of_prime Othe_subsets_of_card Othe_strict_stabilizer_of Rare_conjugated_under Ris_fixed_under Ris_p-group_of_prime Ris_Sylow_p-subgroup_of_prime Vbeing_left_operation #GROUP_2 G0 K0 L0 M1 O6 R0 U0 V0 MSubgroup O(1). 128 Ocarr 128 OLeft_Cosets 128 ORight_Cosets 128 OIndex 128 Oindex 128 #GROUP_3 G0 K0 L0 M0 O3 R2 U0 V1 OSubgroups 124 Rare_conjugated Rare_not_conjugated Ocon_class 124 Vnormal ONormalizator 123 #GROUP_4 G0 K0 L0 M0 O3 R0 U0 V2 Ogr 124 Vgenerating 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 R3 U0 V3 OCosets 148 OCosOp 148 O./. 100 MHomomorphism O1: 148 Onat_hom 148 OKer 148 OImage 148 Vbeing_monomorphism Ris_monomorphism Vbeing_epimorphism Ris_epimorphism Vbeing_isomorphism Ris_isomorphism #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 GHGrWOpStr MAction MCompositionSeries MGroupWithOperators MStableSubgroup Othe_series_of_quotients_of Othe_schreier_series_of Othe_stable_subgroups_of Othe_stable_subgroup_of Othe_stable_subset_generated_by OCosAc Ris_stable_under_the_action_of Rare_equivalent_under Uaction Vcomposition_series Vjordan_holder Vstrictly_decreasing Vhomomorphic #GRSOLV_1 G0 K0 L0 M0 O0 R0 U0 V1 Vsolvable #GR_CY_1 G0 K0 L0 M0 O4 R0 U0 V0 OSegm Oaddint 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 V6 Vc=-linear 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 Ris_a_system_of_different_representatives_of VHall OCut MReduction MSinglification #HAUSDORF G0 K0 L0 M0 O1 R0 U0 V0 OHausDist #HELLY G0 K0 L0 M2 O3 R0 U0 V1 Vwith_Helly_property O.pathBetween 96 OMiddleVertex OmaxPrefix M_Tree M_Subtree #HENMODEL G0 K0 L0 M1 O3 R0 U0 V2 MHenkin_interpretation Omin* OHCar OvalH VConsistent VInconsistent #HERMITAN G0 K0 L0 M4 O7 R0 U0 V7 ODKer OQcFunctional Osignnorm Oquasinorm ORQ*Form OQ*Form OScalarForm Vcmplxhomogeneous VcmplxhomogeneousFAF Vhermitan VdiagRvalued VdiagReR+0valued VdiagReR+valued Vpositivediagvalued Msesquilinear-Form Mone&half-linear-Form Mhermitan-Form Mantilinear-Functional #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 G2 K1 L1 M5 O5 R7 U2 V2 MAny MElement MSubset MReal MNat K[: L:] Obool 128 OREAL 255 ONAT 255 O+ 32 O* R<> Rin Rc= R<= R>= R< R> Vstrict Vempty Ucarrier UZero G1-sorted GZeroStr #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 VHurwitz OF* Odeg Orpoly Oqpoly OCoeff #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 R1 U0 V4 OProjectiveLines OProj_Inc OIncProjSp_of Rare_mutually_different Vpartial Vup-2-dimensional Vup-3-rank MIncProjSp V3-dimensional #INCSP_1 G2 K0 L0 M4 O2 R3 U6 V10 GIncProjStr UPoints ULines UInc GIncStruct UPlanes UInc2 UInc3 MPOINT MLINE MPLANE Ron Vlinear Ris_collinear Vplanar Ris_coplanar VIncSpace-like MIncSpace OLine 15 OPlane 15 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 Vinc-compatible #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 O8 R5 U0 V1 Ris_right_ext_Riemann_integrable_on Ris_left_ext_Riemann_integrable_on Ris_ext_Riemann_integrable_on Oext_right_integral Oext_left_integral Oext_integral Ris_+infty_ext_Riemann_integrable_on Ris_-infty_ext_Riemann_integrable_on Oinfty_ext_right_integral Oinfty_ext_left_integral OOne-sided_Laplace_transform Oexp*- Vinfty_ext_Riemann_integrable Oinfty_ext_integral #INTEGR15 G0 K0 L0 M2 O1 R0 U0 V0 Mmiddle_volume Mmiddle_volume_Sequence Omiddle_sum #INTEGR1C G0 K0 L0 M1 O1 R0 U0 V1 VC1-curve-like MC1-curve OR2-to-C #INTEGRA1 G0 K0 L0 M2 O13 R1 U0 V4 Vclosed-interval MDivisionPoint Odivs MDivision Odivset Oupper_volume Olower_volume Oupper_sum Olower_sum Oupper_sum_set Olower_sum_set Vupper_integrable Vlower_integrable Oupper_integral Olower_integral Ris_integrable_on Ointegral Oindx OPartSums Vintegrable #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 R0 U0 V0 K[' L'] #INTEGRA7 G0 K0 L0 M0 O1 R1 U0 V0 Ris_integral_of OIntegralFuncs #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 O_\/_ O_/\_ O_\_ ORS ORoughSets ORSLattice OERS OInter MIntervalSet O``2 80 OInterLatt OIntervalSets Vordered #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 VIPC_theory VCPC_theory VMC-closed VS4_theory ONes OCnIPC OIPC-Taut Oneg OIVERUM OCnCPC OCPC-Taut OMC-wff OCnS4 OS4-Taut MMC-formula #INT_1 G0 K2 L2 M1 O2 R1 U0 V1 OINT 255 Vinteger MInteger Rare_congruent_mod K[\ L/] K[/ L\] Ofrac 140 #INT_2 G0 K0 L0 M0 O2 R0 U0 V0 Olcm' 32 Ogcd 32 #INT_3 G0 K0 L0 M2 O4 R0 U0 V1 Omultint Ocompint 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 Ris_quadratic_residue_mod OPoly-INT OLege #INT_6 G0 K0 L0 M2 O1 R0 U0 V2 Oto_int VChinese_Remainder Vmultiplicative-trivial MCR_Sequence MCR_coefficients #INT_7 G0 K0 L0 M0 O3 R0 U0 V1 OZ/Z* Omultint0 OSegm0 Vprime-factorization-like #IRRAT_1 G0 K0 L0 M0 O6 R0 U0 V1 Virrational O.^. 120 Oaseq 250 Obseq 250 Ocseq 250 Odseq 250 Oeseq 250 #ISOCAT_1 G0 K0 L0 M1 O0 R2 U0 V0 Ris_equivalent_with Rare_equivalent 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 V1st_class Vwith_1st_class_subsets V2nd_class Vwith_2nd_class_subsets V3rd_class Vwith_3rd_class_subsets Rare_c=-incomparable #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 OFanW OFanN OFanE OFanS O-FanMorphW 101 O-FanMorphN 101 O-FanMorphE 101 O-FanMorphS 101 ONormF 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 ODiskProj ORotateCircle OdiffX2_1 OdiffX2_2 OdiffX1_X2_1 OdiffX1_X2_2 OProj2_1 OProj2_2 #JORDAN1 G0 K0 L0 M0 O0 R1 U0 V2 Vconvex VJordan Rhas_property_J #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 O3 R2 U0 V0 OSouth-Bound ONorth-Bound Rare_neighbours_wrt R-separate O-arc_omitting #JORDAN19 G0 K0 L0 M0 O4 R0 U0 V0 ONorth_Arc OSouth_Arc OUpper_Appr OLower_Appr #JORDAN1A G0 K0 L0 M0 O5 R0 U0 V0 OCenter Onorth_halfline Oeast_halfline Osouth_halfline Owest_halfline #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 #JORDAN1K G0 K0 L0 M0 O2 R0 U0 V0 OLower_Middle_Point OUpper_Middle_Point #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 OUMP OLMP Vwith_the_max_arc #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 O5 R2 U0 V2 Vn_convex VBounded Ris_inside_component_of Ris_outside_component_of OBDD OUBD O1* O1.REAL ORAC #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 O9 R0 U0 V0 Ox_Middle Oy_Middle OL_Segment OR_Segment OSegment OVertical_Line OHorizontal_Line OUpper_Arc OLower_Arc #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 MSegmentation OEucl_dist OS-Gap #KNASTER G0 K0 L0 M0 O5 R1 U0 V0 Ris_a_fixpoint_of Olfp Ogfp O+. O-. OFixPoints #KOLMOG01 G0 K0 L0 M2 O6 R1 U0 V0 OIndep MManySortedSigmaField Ris_independent_wrt MSigmaSection OsigUn OfutSigmaFields OtailSigmaField OfinSigmaFields OMeetSections #KURATO_1 G0 K0 L0 M0 O6 R0 U0 V2 OKurat14Set OKurat7Set OKurat14Part OKurat14ClPart OKurat14OpPart OKurExSet VCl-closed VInt-closed #KURATO_2 G0 K0 L0 M0 O3 R0 U0 V0 OLim_inf OLim_sup OLim_K #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 OMinor OCofactor OLaplaceExpC OLaplaceExpL ORem OMatrix_of_Cofactor OReplaceCol ORCol #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 M4 O13 R2 U0 V1 OEqRelLATT 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 O4 R2 U2 V14 G/\-SemiLattStr UL_meet G\/-SemiLattStr UL_join GLattStr O"\/" O"/\" R[= 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 Vbounded M01_Lattice OBottom 129 OTop 129 Ris_a_complement_of Vcomplemented MC_Lattice VBoolean MB_Lattice #LEXBFS G0 K0 L0 M6 O15 R0 U0 V7 MLexBFS:Labeling MLexBFS:LabelingSeq MpreVNumberingSeq Vvertex-numbering MVNumberingSeq O``1 MMCS:Labeling MMCS:LabelingSeq O.\/ OLexBFS:Init OLexBFS:PickUnnumbered OLexBFS:Update OLexBFS:Step OLexBFS:CSeq OMCS:Init OMCS:PickUnnumbered OMCS:LabelAdjacent OMCS:Update OMCS:Step OMCS:CSeq O.incSubset O.PickedAt Vnatsubset-yielding Vwith_property_L3 Vwith_finite-elements Vwith_property_T Viterative Veventually-constant #LFUZZY_0 G0 K0 L0 M0 O2 R8 U0 V0 ORealPoset R<<= R>>= RR= RR 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_4 G0 K0 L0 M1 O0 R0 U0 V0 MSubmodule #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 OBoundedLinearOperators OR_VectorSpace_of_LinearOperators OR_VectorSpace_of_BoundedLinearOperators OBoundedLinearOperatorsNorm OPreNorms Omodetrans OR_NormSpace_of_BoundedLinearOperators MRealBanachSpace #LOPBAN_2 G1 K0 L0 M3 O6 R0 U0 V4 OFuncMult OFuncUnit OFuncMultBL ORing_of_BoundedLinearOperators MBLAlgebra OR_Algebra_of_BoundedLinearOperators GNormed_AlgebraStr MBanach_Algebra OR_Normed_Algebra_of_BoundedLinearOperators VBanach_Algebra-like MNormed_Algebra VBanach_Algebra-like_1 VBanach_Algebra-like_2 VBanach_Algebra-like_3 #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 O16 R1 U0 V1 OL1_Functions Ra.e.= ORLSp_L1Funct OAlmostZeroFunctions ORLSp_AlmostZeroFunct OPre-L-Space OL-1-Norm OL-1-Space ORLSp_PFunct ORealPFuncZero ORealPFuncAdd ORealPFuncMult ORealPFuncUnit ORealPFuncExtMult Oa.e-eq-class Omultpfunc Omultrealpfunc Vmulti-closed #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 O6 R0 U0 V2 Vrelation-like Mrelation Mrelation_length Orelations_on Oempty_rel OBOOLEAN OFALSE OTRUE Vboolean OALL #MATHMORP G0 K0 L0 M0 O7 R0 U0 V0 O(-) 32 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 OReplaceLine ORLine OPart_sgn O2Set 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 OMX2FinS OFinS2MX Vwithout_repeated_line #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 Vline_circulant Ris_line_circulant_about Vfirst-line-of-circulant Vcol_circulant Ris_col_circulant_about Vfirst-col-of-circulant OLCirc OCCirc Vcirculant Vfirst-line-of-anti-circular Ris_anti-circular_about Vanti-circular OACirc #MATRIXC1 G0 K0 L0 M0 O8 R0 U0 V0 O@" OFinSeq2Matrix OMatrix2FinSeq OLineSum OColSum OQuadraticForm OSumAll OFR2FC #MATRIXJ1 G0 K0 L0 M2 O3 R0 U0 V2 VMatrix-yielding VSquare-Matrix-yielding OLen OWidth Oblock_diagonal MFinSequence_of_Matrix 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 Vempty-yielding MMatrix OIndices OCol O-Matrices_over MDiagonal O-G_Matrix_over #MATRIX_2 G0 K0 L0 M3 O8 R1 U0 V6 O][ 100 MUpper_Triangular_Matrix MLower_Triangular_Matrix ODel ODelCol ODelLine ODeleting Vpermutational OPermutations OGroup_of_Perm Mpermutation Vbeing_transposition Ris_transposition Veven Vodd OFinOmega Vupper_triangular Vlower_triangular #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 R2 U0 V3 Ris_reverse_of Ris_permutable_with VReversible Vsymmetrical VOrthogonal #MATRIX_7 G0 K0 L0 M0 O1 R1 U0 V0 OIFIN Rbeing_Diagonal #MATRIX_8 G0 K0 L0 M0 O0 R2 U0 V4 VIdempotent VNilpotent VInvolutory VSelf_Reversible Ris_similar_Matrix_of Ris_congruent_Matrix_of #MATRIX_9 G0 K0 L0 M0 O1 R0 U0 V0 OPPath_product #MATRLIN G0 K0 L0 M1 O2 R0 U0 V2 VFinSequence-yielding Vfinite-dimensional MOrdBasis Olmlt OAutMt #MATRLIN2 G0 K0 L0 M0 O2 R0 U0 V0 OAutEqMt OMx2Tran #MATROID0 G0 K0 L0 M3 O4 R3 U0 V5 Rc/= Vwith_exchange_property Vfinite-membered Vfinite-degree MSubsetFamilyStr Othe_family_of Vdependent MMatroid OLinearlyIndependentSubsets Ris_maximal_independent_in Ris_dependent_on Vcycle OProdMatroid MDecreasingSequence ORnk #MATRPROB G0 K0 L0 M0 O2 R0 U0 V6 Vm-nonnegative Vwith_sum=1 Vwith_line_sum=1 VProbFinS VJoint_Probability VConditional_Probability ORow_Marginal OColumn_Marginal #MCART_1 G0 K0 L0 M0 O4 R0 U0 V0 O`1 255 O`2 255 O`3 255 O`4 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 M6 O0 R1 U0 V2 MMeasure Ris_measurable Mmeasure_zero MN_Sub_set_fam Vsigma_Field_Subset-like Msigma_Field_Subset MSep_Sequence Msigma_Measure Vsigma-additive #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 Ovol #MEASURE6 G0 K0 L0 M0 O2 R0 U0 V0 OR_EAL O^^ #MEASURE7 G0 K0 L0 M1 O4 R0 U0 V0 MInterval_Covering OSvc OOS_Meas OLmi_sigmaFIELD OL_mi #MEASURE8 G0 K0 L0 M3 O3 R0 U0 V1 MSep_FinSequence MSet_Sequence MCovering OC_Meas OInvPairFunc OVolume Vcompletely-additive #MEMBERED G0 K0 L0 M0 O0 R0 U0 V6 Vcomplex-membered Vreal-membered Vrational-membered Vinteger-membered Vnatural-membered Vext-real-membered #MEMBER_1 G0 K0 L0 M0 O2 R0 U0 V0 O-- 32 O/// #MESFUN10 G0 K0 L0 M0 O0 R1 U0 V1 Vuniformly_bounded Ris_uniformly_convergent_to #MESFUNC1 G0 K0 L0 M0 O7 R1 U0 V0 OINT- ORAT_with_denominator Ris_measurable_on Oless_dom Oless_eq_dom Ogreat_dom Ogreat_eq_dom Oeq_dom #MESFUNC2 G0 K0 L0 M1 O0 R2 U0 V0 Ris_finite 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 MExtREAL_sequence Ointegral+ OIntegral OIntegral_on Vconvergent_to_finite_number Vconvergent_to_+infty Vconvergent_to_-infty Ointegral' Vnonpositive Vwithout+infty Vwithout-infty #MESFUNC7 G0 K0 L0 M0 O2 R0 U0 V1 OExtPower 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 O9 R2 U1 V1 GMidStr UMIDPOINT Oop2 110 OExample 16 VMidSp-like MMidSp R@@ R## OID 128 Ovect 32 Osetvect Oaddvect Ocomplvect Ozerovect Ovectgroup #MIDSP_2 G1 K0 L0 M1 O4 R2 U2 V2 ODouble Rare_associated_wrp Ris_atlas_of Vmidpoint_operator OHalf OAtlas OMidSp. GAtlasStr Ualgebra Ufunction VATLAS-like MATLAS #MIDSP_3 G1 K0 L0 M2 O1 R5 U1 V1 Osub GReperAlgebraStr Ureper MTuple Vbeing_invariance Ris_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 O51 R3 U11 V4 Oatom. VExistNext VExistGlobal VExistUntill OEX OEG OEU OCTL_WFF Oatomic_WFF VCTL-formula-like MCTL-formula Minf_path O|** Ok_id Ok_nat GKripkeStr GCTLModelStr UWorlds UStarts UPossibles UBasicAssign UAssignations ULabel UAnd UNot UEneXt UEGlobal UEUntill OEvaluate MAssign OCTL_WFFS OModelSP OFid OAnd_0 OAnd_ ONot_0 ONot_ OEneXt_univ OEneXt_0 OEneXt_ OEGlobal_univ OEGlobal_0 OEGlobal_ OEUntill_univ OEUntill_0 OEUntill_ OF_LABEL OLabel_ OKModel OCTLModel R|/= OSIGMA OTau OFax OSigFaxTau OUnivF OPrePath OFoax OSigFoaxTau OPathShift OPathChange OPathConc OCastBool OCastboolean OTransEG OTransEU OPred Ris-Evaluation-for Ris-PreEvaluation-for OEvalSet OEvalFamily OCastCTLformula OCastEval OGraftEval #MODELC_2 G1 K0 L0 M1 O24 R0 U4 V4 Vnext VUntil VRelease O'X' O'U' O'R' OLTL_WFF VLTL-formula-like MLTL-formula OCastLTL GLTLModelStr UOr UNEXT UUNTIL URELEASE Oatomic_LTL OLTL_WFFS OInf_seq OCastSeq OOr_ ONext_univ ONext_0 ONext_ OUntil_univ OUntil_0 OUntil_ ORelease_ OLTLModel OAtomicFamily OAtomicFunc OAtomicAsgn OAtomicBasicAsgn OAtomicKai OCastNat #MODELC_3 G2 K0 L0 M0 O23 R7 U3 V3 Vneg-inner-most GLTLnode ULTLold ULTLnew ULTLnext OLTLNew1 OLTLNew2 OLTLNext OCastNode OSuccNode1 OSuccNode2 OSeed OFinalNode OLTLStates OLTLNodes Ris_succ1_of Ris_succ2_of Ris_succ_of Ris_Finseq_for Vfailure Velementary Ris_next_of OPartial_seq OLength_fun GBuchiAutomaton Ris-accepted-by ONeg_atomic_LTL OTran_LTL Ochosen_formula Ochosen_succ Ris_succ_homomorphism Ochoice_succ_func OInitS_LTL OFinalS_LTL OBAutomaton Ochosen_succ_end_num Ochosen_next Ochosen_run #MOD_2 G1 K0 L0 M1 O7 R0 U0 V1 OTrivialLMod GLModMorphismStr 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 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 Vantimultiplicative #MOEBIUS1 G0 K0 L0 M0 O6 R0 U0 V2 OMoebius 128 OSMoebius 128 Vsquare-containing Vsquare-free ONatDivisors OSCNAT ORadical OPFactors #MONOID_0 G0 K0 L0 M4 O19 R0 U0 V7 Vconstituted-Functions Vconstituted-FinSeqs O(*) 128 Vleft-invertible Vright-invertible Vleft-cancelable Vright-cancelable Vuniquely-decomposable MMonoid MMonoidalExtension MSubStr MMonoidalSubStr O[*] O O O Oaddnat O O O Omultnat 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 M0 O8 R0 U0 V0 Ocoprod ODTConMSA OFreeSort ODenOp OFreeOper OFreeMSA OFreeGen OReverse #MSAFREE1 G0 K0 L0 M0 O2 R0 U0 V0 OFlatten OSingleAlg #MSAFREE2 G0 K0 L0 M2 O7 R0 U0 V4 MVertex 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 V4 MMSSubsetFamily Vabsolutely-additive Vabsolutely-multiplicative Vproperly-upper-bound Vproperly-lower-bound #MSUALG_1 G3 K0 L0 M3 O11 R0 U5 V1 MComponent O*--> GManySortedSign UOperSymbols UArity UResultSort MSortSymbol MOperSymbol Othe_result_sort_of Gmany-sorted USorts GMSAlgebra UCharact OArgs ODen Vsegmental OMSSign OMSSorts OMSCharact OMSAlg Othe_sort_of Othe_charact_of O1-Alg #MSUALG_2 G0 K0 L0 M3 O7 R0 U0 V1 MManySortedSubset MMSSubset Vall-with_const_op MMSSubAlgebra OSubSort OMSSubSort OGenMSAlg OMSSub OMSAlg_join OMSAlg_meet OMSSubAlLattice #MSUALG_3 G0 K0 L0 M0 O3 R0 U0 V2 V"1-1" V"onto" O** O"" O.:.: #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 O6 R1 U0 V3 Vfeasible OTranslationRel Otransl 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 VBasis_sigma_discrete VBasis_sigma_locally_finite Vuncountable Ris_a_pseudometric_of #NAGATA_2 G0 K0 L0 M0 O1 R0 U0 V0 OPairFunc #NATTRA_1 G0 K0 L0 M4 O4 R4 U0 V1 Ris_transformable_to 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 M0 O2 R0 U0 V0 Odiv 32 Omod 32 #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 OEuler_phi OEXP #NAT_LAT G0 K0 L0 M3 O12 R0 U0 V0 Ohcflat Olcmlat O0_NN O1_NN ONat_Lattice ONATPLUS MNatPlus Ohcflatplus Olcmlatplus ONatPlus_Lattice MSubLattice OSetPrimes MPrime OSetPrimenumber Oprimenumber #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 O-SuccRelStr OSymRelStr ONecklace Vparallel OComplRelStr #NECKLA_2 G0 K0 L0 M0 O4 R0 U0 V1 VN-free Osum_of Ounion_of Ofin_RelStr Ofin_RelStr_sp #NECKLA_3 G0 K0 L0 M1 O1 R0 U0 V1 Vpath-connected Mpath Ocomponent #NET_1 G1 K0 L0 M1 O11 R3 U3 V1 GNet UPlaces UTransitions UFlow VPetri Ris_Petri_net OElements MPnet Rpre Rpost OPre OPost Oenter Oexit OPrec OPostc OEntr OExt OInput OOutput #NEWTON G0 K0 L0 M0 O3 R0 U0 V0 Ochoose OIn_Power ONewton_Coeff #NORMFORM G0 K0 L0 M0 O5 R0 U0 V0 OFinPairUnion 100 ODISJOINT_PAIRS 100 ONormal_forms_on 110 Omi 110 ONormForm 110 #NORMSP_1 G2 K1 L1 M2 O0 R0 U1 V1 GNORMSTR Unorm K||. L.|| VRealNormSpace-like MRealNormSpace Msequence GNormStr #NORMSP_2 G0 K0 L0 M0 O4 R0 U0 V0 Odistance_by_norm_of OMetricSpaceNorm OTopSpaceNorm OLinearTopSpaceNorm #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 G1 K0 L0 M6 O3 R4 U0 V44 GOrthoRelStr ROrthoComplement_on ROcompl_on RAntitone_on RQuasiOrthoComplement_on OTrivAsymOrthoRelStr OTrivOrthoRelStr OTrivPoset MOrthoPoset MPreOrthoLattice MPreOrthoPoset MPureOrthoRelStr MQuasiOrthoPoset MQuasiPureOrthoRelStr VAntisymmetric VAntitone VAsymmetric Vdneg VDneg VDNeg VOrderInvolutive VOrderinvolutive Vinvolutive VIrreFlexive VPartialordered VPartialOrdered VPreordered VPreOrdered VPure VQuasiordered VQuasiOrdered VOcompl VOrthocomplemented VQuasiOrthocomplemented VQuasiPure VReFlexive VRelAntisymmetric VRelAsymmetric VRelIrreFlexive VRelReFlexive VStrictordered VStrictOrdered VStrictpartialordered VStrictPartialOrdered VSubAntisymmetric VSubAsymmetric VSubIrreFlexive VSubPartialordered VSubPartialOrdered VSubPreOrdered VSubPreordered VSubpreordered VSubQuasiordered VSubQuasiOrdered VSubReFlexive VSubStrictPartialOrdered VSubSymmetric VSubTransitive #OPPCAT_1 G0 K0 L0 M1 O4 R0 U0 V0 Oopp 128 O/* 128 MContravariant_Functor Oid* 128 O*id 128 #ORDERS_1 G1 K0 L0 M5 O5 R0 U1 V1 MChoice_Function OBOOL 122 VOrder-like MOrder GRelStr UInternalRel MPoset MChain OUpperCone 122 OLowerCone 122 OInitSegm 122 MInitial_Segm OChains 122 #ORDERS_2 G0 K0 L0 M0 O0 R12 U0 V3 Vbeing_quasi-order Ris_quasi-order Vbeing_partial-order Ris_partial-order Vbeing_linear-order Ris_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_3 G0 K0 L0 M1 O3 R0 U0 V2 Vdisconnected VPOSet_set-like MPOSet_set OMonFuncs OPOSCat OPOSAltCat #ORDERS_4 G0 K0 L0 M0 O0 R1 U0 V0 Rform_upper_lower_partition_of #ORDINAL1 G0 K0 L0 M2 O1 R0 U0 V5 Osucc 128 Vepsilon-transitive Vepsilon-connected Vordinal MOrdinal Vlimit_ordinal VT-Sequence-like MT-Sequence #ORDINAL2 G0 K0 L0 M1 O13 R1 U0 V4 Olast 128 OOn 128 OLim 128 Oone 128 Oomega 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 Vnatural #ORDINAL3 G0 K0 L0 M0 O3 R0 U0 V0 O-^ 32 Odiv^ 32 Omod^ 32 #ORDINAL4 G0 K0 L0 M0 O3 R0 U0 V0 O0-element_of 128 OZeroMap O1-element_of 128 #ORDINAL5 G0 K0 L0 M0 O5 R0 U0 V3 O|^|^ Ofirst_epsilon_greater_than Oepsilon_ Vepsilon OSum^ VCantor-component VCantor-normal-form O-exponent #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 O9 R3 U1 V3 Odiagonal_o Odiagonal_er UOverloading GRelSortedSign GOverloadedMSSign GOverloadedRSSign Vorder-sorted Vdiscernable OOSSign Vop-discrete 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 V1 MOrderSortedSubset MOSSubset MOSSubAlgebra OOSConstants OOSCl OOSbool OOSSubSort OOSMSubSort Vopers_closed_os 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 OOSQuotCharact OOSQuotArgs 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 R2 U0 V1 VFanodesSp-like MFanodesSp Rparallelogram Rcongr #PARTFUN1 G0 K1 L1 M1 O2 R1 U0 V1 MPartFunc K<: L:> Vtotal OPFuncs 128 Rtolerates OTotFuncs 128 #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 K0 L0 M1 O0 R2 U0 V0 MManySortedSet Roverlaps Rdoes_not_overlap #PCOMPS_1 G0 K0 L0 M0 O5 R1 U0 V3 O1TopSp 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 Gpcs-Str UToleranceRel Vpcs-compatible Vpcs-like Vanti-pcs-like R(--) Mpcs Manti-pcs Opcs-total Opcs-empty Opcs-singleton Opcs-sum Opcs-union Vpcs-yielding GTolStr Opcs-ToleranceRels Opcs-InternalRels VTolStr-yielding Vpcs-tol-total Vpcs-tol-reflexive Vpcs-tol-symmetric OemptyTolStr OMSSet Vtransitive-yielding Vpcs-tol-reflexive-yielding Vpcs-tol-irreflexive-yielding Vpcs-tol-irreflexive Vpcs-tol-symmetric-yielding Vpcs-Str-yielding Vpcs-chain-like Mpcs-Chain Opcs-extension Opcs-reverse Opcs-times K[^ L^] Vpcs-self-coherent Opcs-general-power Opcs-general-power-IR Opcs-general-power-TR Vpcs-self-coherent-membered O^`1 O^`2 Opcs-coherent-power Opcs-power #PDIFF_1 G0 K0 L0 M0 O4 R2 U0 V0 Ris_partial_differentiable_in Ris_partial_differentiable_on Opartdiff Oreproj O`partial| O<>* #PDIFF_2 G0 K0 L0 M0 O4 R2 U0 V0 OSVF1 Opartdiff1 O`partial1| O`partial2| Ris_partial_differentiable`1_on Ris_partial_differentiable`2_on #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 Ohpartdiff21 Ohpartdiff12 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| #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 M6 O8 R0 U2 V2 GColored_PT_net_Str Ocylinder0 OExtcylinders ORistcylinders OCylinderFunc Mthin_cylinder Othin_cylinders Oloc Ufiring-rule UColoredSet MColored-PT-net Mcolor-count Mcolored-state VColored-PT-net-like Voutbound Mconnecting-mapping Mconnecting-firing-rule OOutbds 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 O6 R0 U0 V0 OPolynom OPoly1 OPoly2 OQuard OPoly3 OTri #POLYEQ_2 G0 K0 L0 M0 O2 R0 U0 V0 OFour OFour0 #POLYEQ_3 G0 K0 L0 M0 O2 R0 U0 V0 OPoly_3 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 O25 R0 U2 V7 Mincidence-matrix Mpolyhedron O-polytopes O-chains Vpolyhedral O-chain-space O-boundary O-circuits Vbounding O-bounding-chains O-bounding-circuits O-circuit-space O-bounding-chain-space O-bounding-circuit-space Vsimply-connected Veulerian Onum-polytopes Oalternating-f-vector Oproper-f-vector Oalternating-semi-proper-f-vector Oalternating-proper-f-vector OBoundary Oincidence-sequence O-th-polytope Oincidence-value O-polytope-seq Oeta Opolytopes Onum-vertices Onum-edges Onum-faces GPolyhedronStr UPolytopsF UIncidenceF Vpolyhedron_1 Vpolyhedron_2 Vpolyhedron_3 #POLYNOM1 G0 K0 L0 M3 O9 R2 U0 V1 Vfinite-support Rhas_finite-support OSupport Rhas_finite-Support Mbag OBags OEmptyBag OBagOrder ONatMinor Odivisors Odecomp 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 Ris_a_root_of Vwith_roots Valgebraic-closed ORoots ONormPolynomial OFPower OPolynomial-Function O`^ #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 Opow Ris_primitive_root_of_degree OmConv OaConv ODFT OVandermonde OVM Oemb #POLYRED G0 K0 L0 M0 O2 R6 U0 V0 Rreduces_to Rtop_reduces_to Ris_irreducible_wrt Ris_in_normalform_wrt Ris_top_reducible_wrt Ris_reducible_wrt OSupport@ OPolyRedRel #POWER G0 K0 L0 M0 O4 R0 U0 V0 O-root 200 Oto_power 120 Olog 200 Onumber_e #PRALG_1 G0 K1 L1 M2 O10 R0 U0 V5 K[[: L:]] OInv 128 OTrivialOp OTrivialOps OTrivial_Algebra VUniv_Alg-yielding V1-sorted-yielding Vequal-signature OComSign VFunction-yielding MManySortedFunction MManySortedOperation Vequal-arity OComAr OEmptySeq OProdOp OProdOpSeq OProdUnivAlg #PRALG_2 G0 K1 L1 M1 O7 R0 U0 V1 Vwith_common_domain ODOM Ocommute OCommute K[| L|] MMSAlgebra-Family OSORTS OOPER O?. OOPS #PRALG_3 G0 K0 L0 M1 O1 R0 U0 V0 Oconst MMSAlgebra-Class #PRELAMB G2 K0 L0 M5 O4 R4 U4 V8 Gtypealg Uleft_quotient Uright_quotient Uinner_product Mtype Obranchdeg 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 O6 R0 U0 V1 OGeoSeq 120 O#N 120 O-Root 120 O#Z 120 O#Q 120 VRational_Sequence-like MRational_Sequence O#R 120 #PRE_CIRC G0 K0 L0 M0 O0 R0 U0 V1 Vlocally-finite #PRE_FF G0 K0 L0 M0 O2 R0 U0 V0 OFib OFusc #PRE_TOPC G1 K0 L0 M4 O1 R1 U1 V3 GTopStruct Utopology VTopSpace-like MTopSpace MPoint Vopen Vclosed Ris_a_cover_of MSubSpace Mmap OCl 128 #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* OIFLGT Ris_an_xrep_of Oinner_prd_prg Rscalar_prd_prg Rvector_minus_prg Rvector_add_prg Rvector_sub_prg #PROB_1 G0 K0 L0 M5 O7 R0 U0 V6 Vcompl-closed MField_Subset MSetSequence OUnion OComplement OIntersection Vnon-increasing Vnon-decreasing MSigmaField MEvent MProbability Osigma Ohalfline OFamily_of_halflines OBorel_Sets Vsigma-multiplicative Vnon-ascending Vnon-descending #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 O@Partial_Intersection OPartial_Union O@Partial_Union OPartial_Diff_Union O@Partial_Diff_Union Vnon-increasing-closed Vnon-decreasing-closed MMonotoneClass Omonotoneclass #PROB_4 G0 K0 L0 M0 O6 R0 U0 V0 OSF2SFS OSFS2SF 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 VRealLinearSpace-yielding VRealNormSpace-yielding MRealLinearSpace-Sequence MRealNormSpace-Sequence MMultOps Omultop 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 O4 R5 U0 V0 OSmallestPartition 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 #QC_LANG1 G0 K0 L0 M7 O14 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 Othe_arity_of 20 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! 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 O4 R0 U0 V0 Ovariables_in 68 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 G1 K0 L0 M1 O8 R4 U3 V1 OProbabilities GQM_Str UObservables UStates UQuantum_Probability OObs OSts OMeas VQuantum_Mechanics-like MQuantum_Mechanics Ris_an_involution_in Ris_a_Quantuum_Logic_on OProp R|- R<==> OPropRel OOrdRel OInvRel #QUANTAL1 G3 K0 L0 M4 O3 R0 U1 V10 Vdirected GQuantaleStr GQuasiNetStr Vwith_left-zero Vwith_right-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 OR_Quaternion OG_Quaternion #QUATERNI G0 K0 L0 M0 O9 R0 U0 V1 OQUATERNION Vquaternion O O ORea OIm1 OIm2 OIm3 O0q O1q #QUOFIELD G0 K0 L0 M0 O18 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 Oquotient 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 MReal-Valued-Random-Variable Oexpect OTrivial-SigmaField OTrivial-Probability #RANKNULL G0 K0 L0 M1 O3 R0 U0 V0 Oim Mlinear-transformation Orank Onullity #RAT_1 G0 K0 L0 M1 O1 R0 U0 V1 ORAT 255 Vrational MRational #RCOMP_1 G0 K2 L2 M1 O0 R0 U0 V0 K[. L.] K]. L.[ MNeighbourhood #RCOMP_3 G0 K0 L0 M2 O0 R0 U0 V0 MIntervalCover MIntervalCoverPts #REALSET1 G0 K0 L0 M5 O2 R2 U0 V3 Ris_in MPreserv O|| 100 Vzeroed Vcomplementable MGroup Vtrivial MDOUBLEDOMAIN Ris_Bin_Op_Preserv MPresv O||| 100 MDnT #REALSET2 G0 K0 L0 M1 O10 R0 U0 V0 Osuppf 199 Oodf 199 Ondf 200 Oomf 188 Onmf 200 MOnePoint Ocompf 201 Orevf 201 Oadd_2 Omult_2 OdL-Z_2 #REALSET3 G0 K0 L0 M0 O2 R0 U0 V0 Oosf 199 Oovf 188 #REAL_3 G0 K0 L0 M1 O15 R0 U0 V1 OSimpleContinuedFraction 110 Oscf 110 Vinteger-yielding Oremainders_for_scf 110 Orfs 110 OEuclidSeq 110 MInteger_Sequence Oconvergent_numerators 110 Oconvergent_denominators 110 Oconvergents_of_continued_fractions 110 Oc_d 110 Oc_n 110 Ococf 110 ObackContinued_fraction 110 Obcf 110 OmodSeq 110 OdivSeq 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 OREAL-NS OEuclid_add OEuclid_mult OEuclid_norm 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 O8 R0 U0 V3 VRelation-like MRelation Odom 128 Orng 128 Ofield 128 O~ 128 O| 100 O.: 100 O" 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 #RELOC G0 K0 L0 M0 O3 R0 U0 V0 OIncAddr OShift ORelocated #RELSET_2 G0 K1 L1 M0 O1 R0 U0 V0 O.:^ K{_{ L}_} #REWRITE1 G0 K0 L0 M2 O2 R15 U0 V9 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 Rhas_diamond_property Vconfluent Vwith_Church-Rosser_property Rhas_Church-Rosser_property Vlocally-confluent Rhas_weak-Church-Rosser_property 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 R1 U0 V0 Rare_fiberwise_equipotent O/^ OMIM 128 #RFINSEQ2 G0 K0 L0 M0 O4 R0 U0 V0 Omax_p Omin_p Osort_d Osort_a #RFUNCT_1 G0 K0 L0 M0 O0 R3 U0 V0 Ris_bounded_above_on Ris_bounded_below_on Ris_bounded_on #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 OQuotientRing Vquasi-prime Vquasi-maximal #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 O4 R1 U0 V0 OSubspaces 154 Ris_the_direct_sum_of MLinear_Compl O|-- 32 OSubJoin 124 OSubMeet 124 #RLTOPSP1 G1 K0 L0 M2 O0 R0 U0 V6 GRLTopStruct Vadd-continuous VMult-continuous MLinearTopSpace Vcircled Vcircled-membered Vconvex-membered Vlocally-convex Mlocal_base #RLVECT_1 G2 K0 L0 M2 O2 R0 U2 V5 GLoopStr Uadd GRLSStruct UMult MVECTOR O0. 128 VAbelian Vadd-associative Vright_zeroed Vright_complementable VRealLinearSpace-like MRealLinearSpace OSum 160 #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 #RMOD_3 G0 K0 L0 M0 O1 R0 U0 V0 OSubmodules #ROBBINS1 G3 K0 L0 M1 O12 R0 U1 V6 GComplLattStr UCompl GOrthoLattStr OTrivComplLat OTrivOrtLat VRobbins VHuntington Vjoin-idempotent OBot 129 Vwell-complemented MpreOrthoLattice OCLatt Vwith_idempotent_element O\delta OExpand O_0 O_1 O_2 O_3 O_4 O\beta Vde_Morgan GComplStr #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 GLattRelStr G\/-SemiLattRelStr G/\-SemiLattRelStr GOrthoLattRelStr Vwith_Top Vmeet-Absorbing Vjoin-Associative Vmeet-Associative Vnaturally_sup-generated Vnaturally_inf-generated MOrtholattice OTrivCLRelStr OTrivLattRelStr O|_| O|^| MRelAugmentation MLatAugmentation MCLatAugmentation O"|^|" O"|_|" #ROBBINS4 G0 K0 L0 M1 O2 R0 U0 V2 Vorthomodular VOrthomodular MOrthomodular_Lattice OB_6 OBenzene #ROUGHS_1 G0 K0 L0 M3 O5 R6 U0 V5 MTolerance_Space MApproximation_Space MRoughSet OLAp OUAp OBndAp OMemberFunc OFinSeqM Vwith_equivalence Vexact Vrough Vdiagonal Vwith_tolerance R_c= Rc=^ R_c=^ R_= R=^ R_=^ #RPR_1 G0 K0 L0 M1 O1 R1 U0 V0 MEl_ev Oprob Rare_independent #RSSPACE G0 K0 L0 M0 O13 R0 U0 V0 Othe_set_of_l2RealSequences OZeroseq Othe_set_of_RealSequences Oseq_id OR_id Ol_add Ol_mult Ol_scalar OAdd_ OMult_ OZero_ OLinear_Space_of_RealSequences Ol2_Space #RSSPACE3 G0 K0 L0 M0 O3 R0 U0 V2 Othe_set_of_l1RealSequences Ol1_Space Ol_norm VCCauchy VCauchy_sequence_by_Norm #RSSPACE4 G0 K0 L0 M0 O7 R0 U0 V0 Othe_set_of_BoundedRealSequences Olinfty_Space Olinfty_norm OBoundedFunctions OR_VectorSpace_of_BoundedFunctions OBoundedFunctionsNorm OR_NormSpace_of_BoundedFunctions #RUSUB_4 G0 K0 L0 M0 O0 R0 U0 V2 VAffine VSubspace-like #RUSUB_5 G0 K0 L0 M0 O2 R1 U0 V0 Ris_parallel_to OOrt_Comp OTopUnitSpace #RVSUM_1 G0 K0 L0 M0 O4 R0 U0 V0 Odiffreal 128 Osqrreal 128 Osqr 128 Omlt 128 #SCMBSORT G0 K0 L0 M0 O3 R0 U0 V0 Obubble-sort OBubble-Sort-Algorithm OSorting-Function #SCMFSA6A G0 K0 L0 M1 O4 R0 U0 V0 MMacro-Instruction ODirected OMacro OInitialized O';' #SCMFSA6B G0 K0 L0 M0 O1 R0 U0 V3 OIExec Vparaclosed Vparahalting Vkeeping_0 #SCMFSA6C G0 K0 L0 M0 O2 R0 U0 V0 OInitialize Oswap #SCMFSA7B G0 K0 L0 M0 O0 R3 U0 V2 Rdoes_not_refer Rdoes_not_destroy Vgood Vhalt-free 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-Instr-Loc 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_4 G0 K0 L0 M0 O1 R0 U0 V0 OSCM+FSA-Stop #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 O6 R1 U0 V0 MpreProgram OComput MAutonomy Rhalts_on OIncrIC OData-Locations OMem-Locations OMemPart Omem-only #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 M1 O1 R1 U0 V1 MProgram-block 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 O2 R0 U0 V0 MState-consisting OComplexity OLifeSpan #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 M1 O1 R0 U0 V4 Vdecreasing Vconstant Vmonotone Vnatural-yielding MSeq_of_Nat O^\ #SEQ_1 G0 K0 L0 M1 O2 R1 U0 V3 MReal_Sequence Vbeing_not_0 Vreal-yielding Ris_not_0 O(#) O/" Vcomplex-yielding #SEQ_2 G0 K0 L0 M0 O0 R0 U0 V3 Vbounded_above Vbounded_below 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 V1 OPartial_Sums 250 Vabsolutely_summable #SERIES_3 G0 K0 L0 M0 O1 R0 U0 V0 OPartial_Product 250 #SETFAM_1 G0 K0 L0 M2 O5 R2 U0 V0 Omeet 128 Ris_finer_than Ris_coarser_than OUNION OINTERSECTION ODIFFERENCE MSubset-Family OCOMPLEMENT MCover #SETLIM_1 G0 K0 L0 M0 O4 R0 U0 V0 Oinferior_setsequence Osuperior_setsequence O@inferior_setsequence O@superior_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 O$$ 80 OFinUnion 150 Osingleton 150 K{. L.} #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 O5 R2 U0 V0 Omin_at Ris_split_at 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 U2 V2 Onat_interval Vonto Vbijective OTWOELEMENTSETS GSimpleGraphStruct USVertices 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 GShefferStr GShefferLattStr GShefferOrthoLattStr Ustroke Vsatisfying_Sheffer_1 Vsatisfying_Sheffer_2 Vsatisfying_Sheffer_3 Vproperly_defined Vlower-bounded' Vupper-bounded' OTop' OBot' Vdistributive' Ris_a_complement'_of O`# 100 Vcomplemented' Vmeet-idempotent OTrivShefferOrthoLattStr #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 O23 R0 U0 V0 OPN OCHK ORHK OProd_complex_n OProd_real_n O!c OExpSeq OCoef OCoef_e OSift OExpan OExpan_e OAlfa OConj Osin Ocos OP_sin OP_cos OP_dt OP_t OPI Oexp_R OrExpSeq #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 O4 R0 U0 V0 Otan Ocot 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 O4 R0 U0 V0 Omin 128 Omax 128 O^2 254 Osqrt 200 #STIRL2_1 G0 K0 L0 M0 O1 R0 U0 V1 Oblock V"increasing #STRUCT_0 G3 K0 L0 M0 O1 R0 U3 V0 UZeroF UOneF GOneStr GZeroOneStr G2-sorted Ucarrier' ONonZero #SUBLEMMA G0 K0 L0 M1 O11 R0 U0 V1 MVal_Sub ONEx_Val OVal_S OCQCSub_& OCQCSub_All OCQCSub_the_scope_of OCQCQuant ORSub1 ORSub2 OSbst Oseq OQScope VCQC-WFF-like #SUBSET_1 G0 K0 L0 M0 O2 R0 U0 V0 O[#] 128 O` 150 #SUBSTLAT G0 K0 L0 M0 O2 R0 U0 V0 OSubstitutionSet OSubstLatt #SUBSTUT1 G0 K0 L0 M2 O25 R1 U0 V7 MCQC_Substitution Msecond_Q_comp OvSUB OCQC_Subst ORestrictSub OBound_Vars ODom_Bound_Vars OSub_Var ONSub OupVar OExpandSub OQSub OQC-Sub-WFF OSub_P OSub_not OSub_& OSub_All OSub_the_arguments_of OSub_the_left_argument_of OSub_the_right_argument_of OSub_the_argument_of OSub_the_bound_of OSub_the_scope_of OS_Bound OQuant OCQC_Sub OCQC-Sub-WFF RPQSub VSub_VERUM VSub_atomic VSub_negative VSub_conjunctive Vquantifiable VSub_universal VQC-Sub-closed #SUBSTUT2 G0 K0 L0 M1 O2 R0 U0 V0 MPATH OQsc OCFQ #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 M6 O7 R1 U0 V3 O+infty 200 V+Inf-like M+Inf O-infty 200 V-Inf-like M-Inf Vext-real OExtREAL MR_eal R<' Mmajorant Mminorant OSetMajorant OSetMinorant Mbool_DOMAIN OSUP OINF #SUPINF_2 G0 K0 L0 M4 O2 R1 U0 V3 Vdenumerable MDenum_Set_of_R_EAL Vnonnegative MPos_Denum_Set_of_R_EAL MNum OSer 200 MSet_of_Series OSUM Ris_sumable Vsummable #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 #S_SIEC G0 K0 L0 M0 O8 R0 U0 V0 Os_transitions Os_places Os_carrier Os_enter Os_exit Os_prox Os_pre Os_post #TARSKI G0 K0 L0 M0 O1 R1 U0 V0 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 O4 R0 U0 V0 Olog_ ODiff_Sequence OTaylor Oln #TAYLOR_2 G0 K0 L0 M0 O1 R0 U0 V0 OMaclaurin #TBSP_1 G0 K0 L0 M0 O1 R0 U0 V1 Vtotally_bounded Odiameter #TDGROUP G0 K0 L0 M3 O3 R1 U0 V2 VTwo_Divisible MTwo_Divisible_Group MUniquely_Two_Divisible_Group O# 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 O4 R0 U0 V0 OHT OHM OHC ORed #TEX_1 G0 K0 L0 M0 O4 R0 U0 V0 Ocobool OADTS ODTS 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 M3 O4 R0 U0 V2 OTotal VTolerance-like MTolerance MTolSet VTolClass-like MTolClass Oneighbourhood OTolSets OTolClasses #TOPALG_1 G0 K0 L0 M0 O6 R0 U0 V0 OLoops OFundamentalGroup ORealHomotopy Opi_1 Opi_1-iso OPaths #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 OFGPrIso OGr2Iso #TOPALG_5 G0 K0 L0 M0 O5 R0 U0 V0 OExtendInt OcLoop OCiso OPrj1 OPrj2 #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 V5 ODer Ris_an_accumulation_point_of Ris_isolated_in Vdense-in-itself Vperfect Vscattered Visolated Odensity Vseparable #TOPGEN_2 G0 K0 L0 M1 O2 R0 U0 V2 MNeighborhood_System Vfinite-weight Vinfinite-weight OChi ODiscrWithInfin #TOPGEN_3 G0 K0 L0 M0 O6 R1 U0 V1 Vpoint-filtered OSorgenfrey-line Ocontinuum Ris_local_minimum_of O-powers OClFinTop O-PointClTop O-DiscreteTop #TOPGEN_4 G0 K0 L0 M0 O2 R1 U0 V8 OBorelSets OTotFam Ris_a_condensation_point_of VF_sigma VG_delta Vall-open-containing Vall-closed-containing VBorel Vclosed_for_countable_unions Vclosed_for_countable_meets VT_1/2 #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 R1 U0 V1 OClosed-Interval-MSpace Vbeing_ball-family Ris_ball-family OR^1 OClosed-Interval-TSpace #TOPREAL1 G0 K0 L0 M0 O3 R3 U0 V5 Ris_an_arc_of OR^2-unit_square OLSeg OL~ Vspecial Vunfolded Vs.n.c. Vbeing_S-Seq Ris_S-Seq Vbeing_S-P_arc Ris_S-P_arc #TOPREAL2 G0 K0 L0 M1 O0 R1 U0 V1 Vbeing_simple_closed_curve Ris_simple_closed_curve MSimple_closed_curve #TOPREAL4 G0 K0 L0 M0 O0 R3 U0 V2 Ris_S-P_arc_joining Vbeing_special_polygon Ris_special_polygon Vbeing_Region Ris_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 OTcircle OTunit_circle OTopen_unit_circle Oc[10] Oc[-10] OCircleMap OIntIntervals 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 R8 U0 V6 Ris_FormalIz_of Ris_automorphism_of Ris_DIL_of VCongrSpace-like MCongrSpace Vpositive_dilatation Ris_CDil Vnegative_dilatation Ris_SDil Vdilatation Ris_Dil Vtranslation Ris_Tr Vcollineation Ris_Col #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 O1 R0 U0 V3 Vfinite-order MLevel O-level VBranch-like MBranch VDecoratedTree-like MDecoratedTree MParametrizedSubset #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 Otree #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 #TRIANG_1 G1 K0 L0 M3 O6 R0 U2 V2 Vwith_non-empty_element OSgmX 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 V1 VT_0 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 O23 R2 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 OSucc_Tran OSuccTuring OZero_Tran OZeroTuring OU3(n)Tran OU3(n)Turing OUnionSt OFirstTuringTran OSecondTuringTran OFirstTuringState OSecondTuringState OFirstTuringSymbol OSecondTuringSymbol OUniontran OUnionTran #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 M2 O4 R0 U0 V1 OEqClass MFamily-Class Vpartition-membered MPart-Family 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 O1 R0 U0 V0 MSubAlgebra-Family OCarr #UNIFORM1 G0 K0 L0 M0 O0 R0 U0 V1 Vuniformly_continuous #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 Opoly_shift Opoly_quotient Ofpoly_mult_root Omultiplicity OBRoots Opoly_with_roots MRbag #URYSOHN1 G0 K0 L0 M2 O6 R0 U0 V0 OR<0 OR>1 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 V1 OValuations_in Vboolean-valued OFOR_ALL Minterpretation OValid #VALUED_0 G0 K0 L0 M0 O0 R0 U0 V6 Vcomplex-valued Vext-real-valued Vreal-valued Vrational-valued Vinteger-valued Vnatural-valued #VALUED_2 G0 K0 L0 M0 O23 R0 U0 V12 Vcomplex-functions-membered Vext-real-functions-membered Vreal-functions-membered Vrational-functions-membered Vinteger-functions-membered Vnatural-functions-membered Vcomplex-functions-valued Vext-real-functions-valued Vreal-functions-valued Vrational-functions-valued Vinteger-functions-valued Vnatural-functions-valued OC_Funcs OC_PFuncs OR_Funcs OR_PFuncs OQ_Funcs OQ_PFuncs OI_Funcs OI_PFuncs ON_Funcs ON_PFuncs OE_Funcs OE_PFuncs O(/) O[/] 128 O<+> O<-> O<#> 128 O 128 O<++> O<--> O<##> 128 O 128 ODOMS #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 OcoeffFunctional Oker OCosetSet OaddCoset OzeroCoset OlmultCoset OVectQuot OQFunctional OCQFunctional #VECTSP11 G0 K0 L0 M2 O1 R0 U0 V1 Vwith_eigenvalues Meigenvalue Meigenvector OUnionKers #VECTSP_1 G6 K0 L0 M6 O7 R0 U3 V8 GGroupStr Oaddreal Ocompreal OG_Real MAbGroup GHGrStr Umult GmultLoopStr Uunity O1_ GmultLoopStr_0 GdoubleLoopStr Vright_unital Omultreal OF_Real Vleft_unital VField-like Vdegenerated MField GVectSpStr Ulmult MScalar MVector Ocomp VVectSp-like MVectSp Vright-distributive VFanoian Valmost_left_invertible MAddGroup #VECTSP_2 G2 K0 L0 M6 O6 R0 U1 V4 Vwell-unital McomRing VdomRing-like MdomRing MSkew-Field GRightModStr Urmult GBiModStr OAbGr OLeftModule ORightModule Oop1 110 Oop0 110 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 #VECTSP_9 G0 K0 L0 M0 O2 R0 U0 V0 Odim OSubspaces_of #WAYBEL10 G0 K0 L0 M1 O6 R0 U0 V0 OClOpers MSystem OClosureSystems OClImageMap Oclosure_op ODsupClOpers OSubalgebras #WAYBEL11 G0 K0 L0 M0 O2 R2 U0 V6 Vinaccessible_by_directed_joins Vinaccessible Vclosed_under_directed_sups Vdirectly_closed Vproperty(S) Rhas_the_property_(S) 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 V7 Vmeet-closed Vjoin-closed 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 R3 U0 V4 Vextra-order Mstrict_chain O-LowerMap Vsatisfying_SIC Rsatisfies_SIC_on Vsatisfying_the_interpolation_property Rsatisfies_the_interpolation_property OSetBelow OSupBelow Ris_inductive_wrt OStrict_Chains Vsup-closed #WAYBEL_0 G1 K0 L0 M5 O9 R4 U1 V17 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 Vprincipal 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 R14 U0 V6 Rex_min_of Rhas_the_min_in Rex_max_of Rhas_the_max_in Ris_minimum_of Ris_maximum_of MConnection VGalois Vupper_adjoint Rhas_a_lower_adjoint Vlower_adjoint Rhas_an_upper_adjoint Vprojection Ris_a_projection_operator Vclosure Ris_a_closure_operator Vkernel Ris_a_kernel_operator Ocorestr Oinclusion Ris_a_Heyting_algebra Ris_a_Boolean_algebra Ris_a_Boolean_lattice #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 R5 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 Rsatisfies_SI Vsatisfying_INT Rsatisfies_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 V6 VOpen Vmeet-irreducible Virreducible 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 O6 R0 U0 V0 Ocentralizer OV-centralizer Oconjugate_Classes OCentralizer O-con_map 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 O1 R0 U0 V0 O'\' #XCMPLX_0 G0 K0 L0 M0 O1 R0 U0 V1 O Vcomplex #XREAL_0 G0 K0 L0 M0 O0 R0 U0 V1 Vzero #XXREAL_2 G0 K0 L0 M2 O0 R0 U0 V2 MUpperBound MLowerBound Vleft_end Vright_end #YELLOW11 G0 K0 L0 M0 O2 R0 U0 V0 ON_5 OM_3 #YELLOW13 G0 K0 L0 M0 O0 R0 U0 V1 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 O8 R0 U0 V6 Othe_value_of Othe_universe_of VHausdorff Vyielding_non-empty_carriers MSubNetStr Msubnet ONetUniv Mnet_set OIterated OOpenNeighborhoods MConvergence-Class OConvergence V(CONSTANTS) V(SUBNETS) V(DIVERGENCE) V(ITERATED_LIMITS) OConvergenceSpace OConstantNet #YELLOW_7 G0 K0 L0 M0 O1 R0 U0 V0 OComplMap #YELLOW_8 G0 K0 L0 M0 O1 R1 U0 V3 VBaire Ris_dense_point_of Vsober OCofinTop V-quasi_basis #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 K0 L0 M0 O0 R3 U0 V0 Rare_c=-comparable Rtick_at Rticks #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 Ris_elementary_subsystem_of OZF-axioms 200 Ris_cofinal_with #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 O24 R5 U0 V11 OVAR 128 MVariable Ox. 200 O'=' 90 O'in' 90 O'not' 82 O'&' 80 OAll 68 OWFF 68 VZF-formula-like MZF-formula Vbeing_equality Ris_equality Vbeing_membership Ris_membership Vnegative Vconjunctive Vuniversal Vatomic O'or' 70 O=> 69 O<=> 69 OEx 68 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_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 V2 MSubclass Vnon-empty VDOMAIN-yielding MDOMAIN-Sequence