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