Mizar-widening-like AdjectiveStr adjectives non-op adjective non- TA-structure adj-map adjs consistent adj-structured types adjs-typed is_applicable_to ast sub TAS-structure sub-map non-absorbing subjected is_properly_applicable_to @--> radix varcl variable vars QuasiLoci quasi-loci a_Type an_Adj a_Term non_op constructor MinConstrSign ConstructorSignature initialized Modes Attrs Constructors kind_of loci_of index_of MaxConstrSign MSVars ground compound expression QuasiTerms quasi-term -trm Non QuasiAdjs quasi-adjective pure QuasiTypes quasi-type the_base_of VarPoset vars-function with_an_operation_for_each_sort with_missing_variables term-transformation substitution valuation irrelevant relevant idval at 128 standardized matches_with unifies are_unifiable are_weakly-unifiable is_a_unification_of is_a_general-unification_of subexpression constrs main-constr args base_exp_of type-distribution set-constr set-type arity-rich even odd is_a_fixpoint_of with_fixpoint without_fixpoints covering =_ ARS reduction <== =01=> =*=> =+=> <=01= <=*= <=+= <=01=> <=*=> <=+=> <<>> >><< <<01>> >>01<< normform normalizable is_normform_of WN SN UN UN* N.F. DIAMOND CONF CR WCR COMP ARS_01 ARS_02 TRSStr TotalTRS (R1) (R2) (R3) (R4) (R5) (R6) (R7) (R8) (R9) (R10) (R11) (R12) (R13) (R14) (R15) sgn AES-Statearray SubBytes InvSubBytes ShiftRows InvShiftRows AddRoundKey SubWord RotWord Op-WXOR Rcon KeyExTemp KeyExpansionX KeyExpansion AES-ENC AES-DEC AES-KeyInitState128 AES-KeyInitState192 AES-KeyInitState256 AES128-ENC AES128-DEC AES192-ENC AES192-DEC AES256-ENC AES256-DEC being_line satisfying_PPAP Pappian satisfying_PAP_1 Desarguesian satisfying_DES_1 satisfying_DES_2 Moufangian satisfying_TDES_1 satisfying_TDES_2 satisfying_TDES_3 translational satisfying_des_1 satisfying_pap satisfying_pap_1 satisfying_DES1 satisfying_DES1_1 satisfying_DES1_2 satisfying_DES1_3 satisfying_DES2 satisfying_DES2_1 satisfying_DES2_2 satisfying_DES2_3 being_plane is_coplanar XFinSequence <% %> <%> 254 ^omega Replace Sgm0 {| |} BinComp with_right_units with_left_units AltCatStr compositional FuncComp quasi-functional semi-functional pseudo-functional EnsCat with_units category idm quasi-discrete pseudo-discrete discrete_category DiscrCat cc= the_hom_sets_of the_comps_of Alter the_empty_category SubCatStr ObCat id-inheriting subcategory is_left_inverse_of is_right_inverse_of iso are_iso mono _zero AllMono AllEpi AllRetr AllCoretr AllIso ObjectsFamily MorphismsFamily projection-morphisms with_products -CatProduct-like EnsCatProductObj EnsCatProduct coprojection-morphisms with_coproducts -CatCoproduct-like EnsCatCoproduct EnsCatCoproductObj Coprod 100 IL-Subset jump-only NIC JUMP SUCC InsLoc-antisymmetric STC il. locnum NextLoc really-closed para-closed LastLoc halt-ending unique-halt pre-Macro jumps_in jump_in JumpParts AddressParts with_explicit_jumps without_implicit_jumps ins-loc-free Stop IncAddr IC-relocable relocable Exec-preserving CutLastLoc Relocated J/A-independent TrivialInfiniteTree FirstLoc LocNums LocSeq ExecTree with_non_trivial_Instructions with_non_trivial_ObjectKinds Out_\_Inp Out_U_Inp IC-recognized CurIns-recognized relocable1 relocable2 -halting AMI-Struct InstructionsF Instructions Object-Kind Execution Trivial-AMI Instruction IC JumpPart ObjectKind Exec halt IC-Ins-separated CurInstr PartState FinPartState ProgramPart halts_on FinPartSt Data-Locations -autonomic Program InsCode AddressPart standard-ins InsCodes InsType Start-At halts_at DataPart data-only halt-free -halted -started SCM-Halt SCM-Data-Loc SCM-Memory SCM-Instr SCM-OK SCM-State SCM-Chg address_1 address_2 jump_address cjump_address cond_address SCM-Exec-Res SCM-Exec SCM-VAL SCM*-VAL Int-like SCM Data-Location AddTo SubFrom MultBy Divide goto SCM-goto =0_goto >0_goto dl. Euclid-Algorithm Euclid-Function weakly_standard Gen are_Ort_wrt Orthogonality OrtStr ParOrtStr orthogonality AMSpace Af OrtAfSp-like OrtAfSp OrtAfPl-like OrtAfPl // AffinStruct CONGR DirPar OASpace OAffinSpace-like OAffinSpace 2-dimensional OAffinPlane Ortm Orte are_COrte_wrt are_COrtm_wrt CORTE CORTM CESpace CMSpace are_Prop are_LinDep Proportionality_as_EqRel_of Dir ProjectivePoints ProjectiveCollinearity ProjectiveSpace are_Prop_Vect lie_on_a_triangle are_perspective lie_on_an_angle are_half_mutually_not_Prop Vebleian at_least_3rank CollProjectiveSpace at_most-3-dimensional CollProjectivePlane nin orbit Generators with_empty-instruction with_catenation with_if-instruction with_while-instruction preIfWhileAlgebra Algorithm EmptyIns \; 16 if-then-else if-then while for-do ElementaryInstructions ECIW-signature ECIW-strict IfWhileAlgebra complying_with_empty-instruction complying_with_catenation complies_with_if_wrt complies_with_while_wrt ExecutionFunction iteration_terminates_for iteration-degree TerminatingPrograms absolutely-terminating is_terminating_wrt is_invariant_wrt -singleton ManySortedMSSet VarMSAlgebra free-vars vf vf-correct vf-free UndefMSAlgebra undefined-map undefined undef-consequent -undef ManySortedElement GeneratorSystem generators supported-var supported-term -supported supp-var supp-term is_of_type ConnectivesSignature connectives -connectives 1-1-connectives BoolSignature bool-sort bool-correct \true \not 124 \and 112 \or 100 \imp 88 \iff 88 \0 \1 the_array_sort_of ProgramAlgStr assignments ProgramAlgebra -States value_at -Execution -array array-correct init.array \2 \false basic integer-array array-degenerated (#INT,<=#) leq 32 gt 32 eq 32 Enumeration Denumeration INT-Variable INT-Expression INT-Array is_assignment_wrt form_assignment_wrt INT-ElemIns INT-Exec += 32 *= 32 swap %= 32 /= 32 is_odd is_even geq 32 lt 32 -tolerating extended_by -vf-yielding with_equality essential VariableSet language PCLangSignature QCLangSignature AlgLangSignature formula-sort program-sort quant-sort quantifiers subst-op equality LanguageStr Formula subst-correct subst-correct2 subst-correct3 subst-forex \true_ \for 128 \ex 128 AL-correct BialgebraStr AlgorithmicLogic PC-correct QC-correct vf-qc-correct 1s-empty ua-non-empty PC-closed QC-closed AL-closed PC-theory QC-theory QC-theory_with_equality AL-theory SubstMSAlgebra sort-preserving subst-eq-correct vf-eq-correct vf-finite \Cup \Cap Maximal_in is_/\-irreducible_in is_/\-reducible_in /\-IRR (B1) (B2) DB-Rel Attributes Domains Relationship Subset-Relation Dependency-set Dependencies Dependency >|> holds_in Dependency-str is_at_least_as_informative_as Dependencies-Order (F2) (DC1) (F1) (DC2) (F3) (F4) full_family Full-family (DC3) Maximal_wrt ^|^ (M1) (M2) (M3) saturated-subsets closed_attribute_subset deps_encl_by enclosure_of Dependency-closure is_generator-set_of candidate-keys (C1) without_proper_subsets (C2) (DC4) (DC5) (DC6) charact_set is_p_i_w_ncv_of LinPreorders LinOrders <=_ >=_ <_ >_ opp 128 inv [* *] -' 32 - 32 DEDEKIND_CUTS REAL+ DEDEKIND_CUT 130 GLUED 130 one 128 are_coprime divides lcm 32 hcf 32 RED RAT+ numerator 150 denominator 150 / quotient + 32 *' 128 <=' < logbase eventually-nonnegative eventually-positive eventually-nonzero eventually-nondecreasing majorizes Big_Oh Big_Omega Big_Theta taken_every is_smooth_wrt smooth seq_a^ seq_logn seq_n^ seq_const seq_n! POWEROF2SET Step1 polynomially-bounded seq_p negligible polynom negligibleFuncs negligibleEQ Big_Oh_poly R_Algebra_of_Big_Oh_poly polynomially-abs-bounded UAAut UAAutComp UAAutGroup MSFunctionSet MSAAut MSAAutComp MSAAutGroup Aut AutComp AutGroup InnAut InnAutGroup Conjugate TotDegree TermOrder LexOrder admissible InvLexOrder Graded GrLexOrder GrInvLexOrder BlockOrder NaivelyOrderedBags PosetMin PosetMax FinOrd-Approx FinOrd FinPoset MinElement multiset RelMultMagma RelMonoid RelExtension DershowitzMannaOrder partition co-ordered OrderedPartition PrecM PrecPrecM Election -dominated-election DominatedElection BCIStr InternalDiff BCIStr_0 being_B being_C being_I being_K being_BCI-4 being_BCK-5 BCI-EXAMPLE 16 BCI-algebra BCK-algebra BCK-part AtomSet generated_by_atom BranchV quasi-associative positive-implicative weakly-positive-implicative weakly-implicative p-Semisimple alternative least greatest nilpotent L-congruence R-congruence I-congruence IConSet ConSet LConSet RConSet EqClaOp zeroEqC being_greatest being_positive BCI-commutative BCI-weakly-commutative involutory being_Iseki Iseki_extension Commutative-Ideal BCK-positive-implicative BCK-implicative BCIStr_1 ExternalDiff with_condition_S BCI_S-EXAMPLE BCI-Algebra_with_Condition(S) Condition_S Adjoint_pGroup Product_S BCK-Algebra_with_Condition(S) Initial_section being_SB-1 being_SB-2 being_SB-4 semi-Brouwerian-algebra quasi-commutative p-Semisimple-part BCI-power 124 finite-period BCI-homomorphism isotonic HKOp zeroHK HK initial_section associative-ideal p-ideal implicative-ideal positive-implicative-ideal UNITSTR scalar RealUnitarySpace-like RealUnitarySpace Cauchy is_compared_to Hilbert setop_SUM Func_Seq setopfunc setop_xPre_PROD setop_xPROD OrthogonalFamily OrthonormalFamily setsum summable_set weakly_summable_set is_summable_set_by sum_byfunc Form NulForm FunctionalFAF FunctionalSAF FormFunctional additiveFAF additiveSAF homogeneousFAF homogeneousSAF bilinear-Form leftker rightker diagker LKer RKer LQForm RQForm QForm degenerated-on-left degenerated-on-right carry Binary Absval add_ovfl are_summable Bin1 Neg2 Intval Int_add_ovfl Int_add_udfl -BinarySequence MajP 2sComplement Nat-mult-left Nat-mult-right UnOp BinOp commutative associative idempotent is_a_left_unity_wrt is_a_right_unity_wrt is_a_unity_wrt the_unity_wrt 128 is_left_distributive_wrt is_right_distributive_wrt is_distributive_wrt compcomplex 128 invcomplex addcomplex 128 diffcomplex 128 multcomplex 128 divcomplex compreal invreal addreal diffreal 128 multreal divreal comprat invrat addrat diffrat multrat divrat compint addint diffint multint addnat multnat root-label binary NumberOnLevel FinSeqLevel -hash Bool_marks_of Boolean_marking is_firable_on is_not_firable_on Firing Base-Appr Pr1 Pr2 TrivDecomp space Proj 128 TrivExt 128 u.s.c._decomposition DECOMPOSITION-like DECOMPOSITION I[01] 0[01] 1[01] being_a_retraction is_a_retract_of is_an_SDR_of are_connected arcwise_connected are_homotopic pathwise_connected I(01) IRRAT RePar 1RP 2RP 3RP LowerLeftUnitTriangle IAA UpperUnitTriangle IBB LowerRightUnitTriangle ICC Homotopy Sn1->Sn 100 with_antipodals without_antipodals Rn->S1 c[100] c[-100] CircleIso 100 are_antipodals_of liftPath SphereMap eLoop Shift_Seq @Shift_Seq Union_Shift_Seq @Union_Shift_Seq @lim_sup Intersect_Shift_Seq @Intersect_Shift_Seq @lim_inf is_all_independent_wrt JSum JSum2 Sum_Shift_Seq Special_Function Special_Function2 Special_Function3 Special_Function4 DiffElems Tdisk HC BR-map Z_2 \*\ bspace-sum bspace-scalar-mult bspace Singleton singletons 'imp' 15 'eqv' 14 O_el 255 I_el 255 B_INF 255 B_SUP 255 is_dependent_of GPart is_upper_min_depend_of generating independent is_a_coordinate CompF is_independent_of All 68 Ex 68 having-inverse additively-closed Subring multiplicatively-closed mult_ One_ additively-linearly-closed scalar-mult-cancelable R_Algebra_of_BoundedFunctions R_Normed_Algebra_of_BoundedFunctions ContinuousFunctions R_Algebra_of_ContinuousFunctions R_Normed_Algebra_of_ContinuousFunctions ContinuousFunctionsNorm C_0_Functions R_VectorSpace_of_C_0_Functions C_0_FunctionsNorm R_Normed_Space_of_C_0_Functions Ant Suc is_tail_of is_Subsequence_of set_of_CQC-WFF-seq is_a_correct_step a_proof is_formal_provable_from seq Per Begin Impl IdFinS UniCl quasi_basis FinMeetCl quasi_prebasis prebasis the_Cantor_set 200 cap-finite-closed Filter_Intersection filter_base Tails_Filter base_of_frechet_filter PLO1 PLO2 PLO2bis filter_basis elementary_filter filter_image is_filter-finer_than is_filter-coarser_than are_equivalent_generators Tails F2BOOL BOOL2F lim_filter lim_f lim_filterb sequence_to_net OrderedFIN Sum_f square-uparrow square-downarrow all-square-uparrow dblseq_ex_1 derangements round der_seq not-one-to-one 0 cardinal Cardinal card 128 nextcard 128 limit_cardinal aleph 128 Segm -element +` 32 *` Cardinal-yielding Cardinal-Function Card 128 disjoin 128 Union product 128 pi 128 Sum 160 Product 128 sproduct with_common_domain DOM product" 128 product-like countable denumerable proj 128 choice Choice Aleph cf -powerfunc_of regular irregular Filter dual Ideal is_multiplicative_with is_additive_with is_complete_with uniform principal being_ultrafilter Extend_Filter Filters Frechet_Filter Frechet_Ideal GCH inaccessible strong_limit strongly_inaccessible measurable predecessor Inf_Matrix is_Ulam_Matrix_of Choose Card_Intersection is_unbounded_in is_closed_in is_club_in unbounded LBound stationary is_stationary_in limpoints Mahlo strongly_Mahlo Catalan dominated_by_0 Domin_0 OMEGA (##) -MSF CatSign Signature CatSignature underlay delta-concrete idsym homsym compsym Upsilon Psi CatStr Comp IdMap Object Morphism Hom 128 Category-like Category 1Cat 255 monic epi terminal initial Functor Obj isomorphic full faithful hom with_identities identity-preserving Functor-like Funct FUNCTOR-DOMAIN Subcategory is_full_subcategory_of ?- 128 -? 128 cods 128 retraction coretraction term 250 init 250 Projections_family is_a_product_wrt Injections_family is_a_coproduct_wrt with_finite_product ProdCatStr TerminalObj CatProd Proj1 Proj2 [1] 250 [x] c1Cat 128 Cartesian Cartesian_category lambda' 128 rho 128 rho' 128 Switch 128 Delta 128 Alpha 128 Alpha' 128 with_finite_coproduct CoprodCatStr Initial Coproduct Incl1 Incl2 in1 128 in2 128 c1Cat* 128 Cocartesian Cocartesian_category [$ $] with_triple-like_morphisms categorial Categorial -SliceCat SliceFunctor SliceContraFunctor CategoryStr composition Mor Ob morphism are_composable |> right_identity left_identity identity right_composable left_composable composable with_left_identities with_right_identities DiscreteCat id- SourceMap TargetMap CompMap alter is_pullback_of pullback section_ preorder -ordered RelOb MORPHISM OrdC is_product_of is_exponent_of is_natural_transformation_of categorical_product categorical_exponent with_binary_products with_exponential_objects with_terminal_objects with_initial_objects ->OrdC1 OrdC0-> COMPOSITION KuratowskiPair [|x|] N_Real Cayley-Dickson binop 110 ConjNormAlgStr conjugateF well-conjugated add-conjugative norm-conjugative scalar-conjugative permutations SymGroup CayleyIso 100 SymGroupsIso 100 ComplexSubAlgebra Cadditively-linearly-closed C_Algebra_of_BoundedFunctions C_Normed_Algebra_of_BoundedFunctions CContinuousFunctions C_Algebra_of_ContinuousFunctions CContinuousFunctionsNorm C_Normed_Algebra_of_ContinuousFunctions CC_0_Functions C_VectorSpace_of_C_0_Functions CC_0_FunctionsNorm C_Normed_Space_of_C_0_Functions is_continuous_on InvShift C_RestFunc C_LinearFunc ComplexFuncAdd ComplexFuncMult ComplexFuncExtMult ComplexFuncZero ComplexFuncUnit CRing ComplexAlgebraStr CAlgebra ComplexAlgebra left-right LeftOptions RightOptions the_LeftOptions_of the_RightOptions_of the_Options_of ConwayDay ConwayGame ConwayGame-like ConwayZero ConwayOne ConwayStar ConwayRank ConwayGame-valued ConwayGameChain-like ConwayGameChain the_Tree_of the_proper_Tree_of fuzzy Grating Gap cells Cell infinite-cell star del bounds GrChain .followSet minlength are_adjacent .AdjacentSet AdjGraph simplicial VertexSeparator minimal chordal chordless VertexScheme stabilizing with_stabilization-limit stabilization-time one-gate with_nonpair_inputs Gate 1GateCircStr unsplit gate`1=arity gate`2isBoolean gate`2=den FinSeqLen 1GateCircuit Circled-Family Cir circled_Combination circledComb -CircuitStr the_action_of -CircuitSorts -CircuitCharact -Circuit CompatibleValuation are_equivalent_wrt preserves_inputs_of form_embedding_of are_similar_wrt calculates specifies SortMap OperMap Circuit Set-Constants InputFuncs -th_InputValues depends_on_in size Fix_inp Fix_inp_ext IGTree IGValue Following stable InitialComp Computation is_continuously_differentiable_up_to_order Ck_Functions R_Algebra_of_Ck_Functions subset-closed Tarski is_Tarski-Class_of Tarski-Class 200 Rank 200 the_transitive-closure_of 128 the_rank_of 200 are_fiberwise_equipotent universal Universe FinSETS 200 SETS 200 Universe_closure FinSet Set UNIVERSE ComplexVectSpace C_VectorSpace_of_LinearOperators C_VectorSpace_of_BoundedLinearOperators C_NormSpace_of_BoundedLinearOperators ComplexBanachSpace C_Algebra_of_BoundedLinearOperators ComplexBLAlgebra Normed_Complex_AlgebraStr C_Normed_Algebra_of_BoundedLinearOperators Normed_Complex_Algebra Complex_Banach_Algebra MSSetOp MSClosureStr MSFull MSClosureSystem MSClosureOperator MSFixPoints in' c=' Bool SubsetFamily SetOp ClosureStr Family Full ClosureSystem ClosureOperator ClOp->ClSys ClSys->ClOp supp MSUnion SubAlgCl CLSStruct ComplexLinearSpace-like Trivial-CLSStruct ComplexLinearSpace CNORMSTR ComplexNormSpace-like ComplexNormSpace FlatCoh Sub_of_Fin c=directed c=filtered d.union-closed includes_lattice_of union-distributive d.union-distributive c=-monotone cap-distributive U-continuous U-stable U-linear graph Trace StabCoh LinTrace LinCoh U+ binary_complete Coherence_Space Web CohSp CSp FuncsC MapsC CDom CCod CComp CId CohCat Toler Toler_on_subsets TOL FuncsT MapsT TolCat Relation3 CollStr Collinearity CollSp PartialLinearSpace G_ clique maximal_clique STAR TOP IncProjMap point-map line-map incidence_preserving incprojmap commaObjs commaMorphs commaComp comma relatively-compact pre-compact liminally-compact locally-relatively-compact locally-closed/compact compactification One-Point_Compactification Re 128 0c 128 1r 128 |. .| abs 150 angle F_Complex abscomplex 128 ComplexOpenSets the_Complex_Space countably_compact well_dist WellSpace pointwise_bounded ComSgn JumpArityF AddressArityF JumpArity AddressArity enumerated ComList with_halt haltF COM-Struct Trivial-COM proper-halt IncIC DecIC Instruction-Sequence MacroInstruction Arg CRoot Hausdorff 1TopSp to-naturals len-total with_the_same_arity HFuncs is_primitive-recursively_expressed_by primrec composition_closed primitive-recursion_closed primitive-recursively_closed PrimRec primitive-recursive initial-funcs PR-closure composition-closure PrimRec-Approximation nullary unary ternary (1,2)->(1,?,2) [!] [^] [pred] -ary Complex_Sequence #N 120 satisfying_DES satisfying_AH satisfying_3H satisfying_ODES satisfying_LIN satisfying_LIN1 satisfying_LIN2 quasi-empty ContextStr Information FormalContext Attribute is-connected-with is-not-connected-with ObjectDerivation AttributeDerivation phi psi co-Galois ConceptStr Extent Intent concept-like FormalConcept co-universal Concept-with-all-Objects Concept-with-all-Attributes Set-of-FormalConcepts is-SubConcept-of is-SuperConcept-of B-carrier B-meet B-join ConceptLattice gamma Context DualHomomorphism satisfying_OPAP satisfying_PAP satisfying_MH1 satisfying_MH2 satisfying_TDES satisfying_SCH satisfying_OSCH satisfying_des satisfying_minor_Scherungssatz satisfying_major_Scherungssatz satisfying_Scherungssatz satisfying_indirect_Scherungssatz satisfying_minor_indirect_Scherungssatz satisfying_major_indirect_Scherungssatz are_separated are_joined is_a_component_of Component_of 128 a_component a_neighborhood is_locally_connected_in locally_connected qComponent_of 128 a_union_of_components Down convex Convex-Family conv Convex_Combination ConvexComb cone C_Linear_Combination ZeroCLC C_LinComb C_LCAdd C_LCMult LC_CLSpace Add_in_Prod_of_RLS Mult_in_Prod_of_RLS Prod_of_RLS RLS_Real epigraph IntervalSequence set_of_tagged_Division delta-fine tagged_division division_of Substitution Subst CQC-WFF 254 CQC-variable_list NEGATIVE CON UNIVERSAL ATOMIC QuantNbr SepFunc NBI index 128 SepVar is_Sep-closed_on SepQuadruples 100 are_similar being_a_theory Cn Proof_Step_Kinds is_a_correct_step_wrt is_a_proof_wrt Effect TAUT |- valid |-| is_an_universal_closure_of the_set_of_ComplexSequences C_id CZeroseq Linear_Space_of_ComplexSequences the_set_of_l2ComplexSequences CUNITSTR ComplexUnitarySpace-like ComplexUnitarySpace cl_scalar Complex_l2_Space ComplexHilbertSpace the_set_of_l1ComplexSequences cl_norm Complex_l1_Space the_set_of_BoundedComplexSequences Complex_linfty_norm Complex_linfty_Space ComplexBoundedFunctions C_VectorSpace_of_BoundedFunctions ComplexBoundedFunctionsNorm C_NormSpace_of_BoundedFunctions P-convergent P-lim convergent_in_cod1 convergent_in_cod2 lim_in_cod1 lim_in_cod2 cod1_major_iterated_lim cod2_major_iterated_lim uniformly_convergent_in_cod1 uniformly_convergent_in_cod2 Row_Series Column_Series Column-major_Partial_Sums Row-major_Partial_Sums Partial_Sums_in_cod2 Partial_Sums_in_cod1 P-convergent_to_finite_number P-convergent_to_+infty P-convergent_to_-infty convergent_in_cod1_to_+infty convergent_in_cod1_to_-infty convergent_in_cod1_to_finite convergent_in_cod2_to_+infty convergent_in_cod2_to_-infty convergent_in_cod2_to_finite alpha-set semi-open pre-open pre-semi-open semi-pre-open sInt pInt alphaInt psInt spInt ^alpha SO PO SPO PSO D(c,alpha) D(c,p) D(c,s) D(c,ps) D(alpha,p) D(alpha,s) D(alpha,ps) D(p,sp) D(p,ps) D(sp,ps) s-continuous p-continuous alpha-continuous ps-continuous sp-continuous (c,alpha)-continuous (c,s)-continuous (c,p)-continuous (c,ps)-continuous (alpha,p)-continuous (alpha,s)-continuous (alpha,ps)-continuous (p,ps)-continuous (p,sp)-continuous (sp,ps)-continuous Op-Left Op-Right SP-Left SP-Right Op-LeftShift Op-RightShift Op-Shift Op-XOR DES-CoDec DES-like-CoDec DES-ENC DES-DEC DES-SBOX1 DES-SBOX2 DES-SBOX3 DES-SBOX4 DES-SBOX5 DES-SBOX6 DES-SBOX7 DES-SBOX8 bitshift_DES DES-IP DES-PIP DES-IPINV DES-PIPINV DES-E DES-P DES-PC1 DES-PC2 DES-DIV8 DES-F DES-FFUNC ntoSeg NtoSEG B6toN64 N16toB4 DES-KS weakly-ascending quasi_ordered <=E \~ min-classes is_Dickson-basis_of Dickson mindex Dickson-bases NATOrd OrderedNAT fD bD cD forward_difference fdif backward_difference bdif central_difference cdif [! !] Sequence-yielding Seq_Sequence Clique StableSet with_finite_clique# clique# with_finite_stability# stability# minimals maximals Clique-wise Clique-partition StableSet-wise Coloring strong-chain F_dp1 Equal_Div_interval lambda Lambda Mid LIN AffinSpace-like AffinSpace AffinPlane '//' Oriented_Orthogonality_Space-like Oriented_Orthogonality_Space bach_transitive right_transitive left_transitive Euclidean_like Minkowskian_like whole_event event_pick frequency FDprobability FDprobSEQ -are_prob_equivalent Finseq-EQclass distribution_family GenProbSEQ distribution freqSEQ distProbFinS uniformly_distributed uniform_distribution Uniform_FDprobSEQ distProbFinS-Family sample samplingRNG well-distributed EqSampleSpaces Prob ProbFinS_of trueEVENT extract MembershipDecision ConditionalSS TS PeanoNat with_terminals with_nonterminals with_useful_nonterminals Terminal NonTerminal SubtreeSeq plus-one PN-to-NAT PNsucc NAT-to-PN TerminalString PreTraversal PostTraversal TerminalLanguage PreTraversalLanguage PostTraversalLanguage LinearFunctionals MultF_Real* MultReal* RLSp2RVSp RVSp2RLSp R_VectorSpace_of_BoundedLinearFunctionals BoundedLinearFunctionalsNorm BoundedLinearFunctionals Bound2Lipschitz DualSp SubRealNormSpace BiDual BidualFunc RNS_Real weakly-convergent w-lim weakly*-convergent w*-lim weakly-sequentially-compact normRU RUSp2RNSp UKer seqIntersection intersection_stable disjointify Dynkin_System generated_Dynkin_System DynSys Subfield GF quadratic_residue not_quadratic_residue Lege_p ProjCo EC_WEqProjCo Disc EC_SetProjCo _EQ_ R_ProjCo R_EllCur _or_greater EC_WParam is_on_curve rep_pt compell_ProjCo addell_ProjCo UAEnd UAEndComp UAEndMonoid MSAEnd MSAEndComp MSAEndMonoid Maps 128 id$ surjective fDom 128 fCod 128 fComp 128 fId 128 Ens 128 hom?- 128 hom-? 128 hom?? 128 has_onlyone_value_in Vec2DiagMx Mx2FinS FinSeq_log Infor_FinSeq_of Entropy Entropy_of_Joint_Prob Entropy_of_Cond_Prob nabla Tolerance Equivalence_Relation "\/" Class a_partition EqClass SmallestPartition Family-Class partition-membered Part-Family Intersection SuperAlgebraSet TermAlg Equations EqualSet absreal 0* Pitag_dist Euclid TOP-REAL 0.REAL |[ ]| the_diameter_of_the_circumcircle being_point half_length the_midpoint_of_the_segment the_perpendicular_bisector the_circumcenter the_radius_of_the_circumcircle the_centroid_of_the_triangle median the_altitude the_foot_of_the_altitude the_length_of_the_altitude the_orthocenter line_of_REAL dist_v plane_of_REAL are_coplane cpx2euc euc2cpx Triangle closed_inside_of_triangle inside_of_triangle outside_of_triangle plane are_lindependent2 are_ldependent2 tricord1 tricord2 tricord3 trcmap1 trcmap2 trcmap3 |{ }| the_area_of_polygon3 the_perimeter_of_polygon3 R-orthogonal R-normal R-orthonormal orthogonal_basis linear_manifold L_Span accum ProjFinSeq RN_Base Orthogonal_Basis VFunc VFuncdiff max_diff_index Intervals OpenHypercube OpenHypercubes Euclidean Homogeneous Euler 128 odd-valued odd_organization Euler_transformation -based -limited base- limit- len- array permutation arr_computation inversions halts_in halt_in is_sequential_in preProgram Comput Autonomy G_Net entrance escape GG gg_net EE e_net empty_e_net Tempty_e_net Pempty_e_net Psingle_e_net Tsingle_e_net PTempty_e_net e_Places e_Transitions e_Flow e_places e_transitions e_pre e_post e_shore e_prox e_flow e_support e_entrance e_escape e_stanchion e_circulation e_adjac s_transitions s_places s_carrier s_enter s_exit s_prox s_pre s_post pair with_pair without_pairs nonpair-yielding or3 is_stable_at 2GatesCircStr 2GatesCircOutput 2GatesCircuit BitAdderOutput BitAdderCirc MajorityIStr MajorityStr MajorityICirc MajorityOutput MajorityCirc BitAdderWithOverflowStr BitAdderWithOverflowCirc SingleMSS SingleMSA -BitAdderStr -BitAdderCirc -BitMajorityOutput -BitAdderOutput is_continuous_in Lipschitzian uniformly_continuous -convergent RestFunc-like RestFunc linear LinearFunc is_differentiable_in diff is_differentiable_on `| differentiable is_Lcontinuous_in is_Rcontinuous_in is_right_differentiable_in is_left_differentiable_in Ldiff Rdiff PTempty_f_net Tempty_f_net Pempty_f_net Tsingle_f_net Psingle_f_net empty_f_net f_enter f_exit f_prox f_flow f_places f_transitions f_pre f_post f_entrance f_escape f_circulation f_adjac Fib_Program Fusc' Fusc_Program tau tau_bar FIB EvenNAT OddNAT EvenFibs OddFibs Lucas GenFib File is_a_record_of <. .) implicative I_Lattice latt 128 equivalence_wrt are_equivalence_wrt /\/ 128 LattRel 128 (. .> max-ideal ElementsOfBuyPortfolio BuyPortfolioExt BuyPortfolio is_random_variable_on pricefunction set_of_random_variables_on ElementsOfPortfolioValue_fut ElementsOfPortfolioValueProb_fut PortfolioValueFutExt PortfolioValueFut Change_Element_to_Func Element_Of half_open_sets halfline_fin RVElementsOfPortfolioValue_fut RVPortfolioValueFutExt_El Subset_of_REAL1 Subset_of_REAL2 GoCross_Seq_REAL GoCross_Partial_Union GoCross_Union Family_of_halflines2 halfline2 RVPortfolioValueFut RVPortfolioValueFutExt Filtration Special_SigmaField1 Special_SigmaField2 Special_SigmaField3 Sigma_of_ManySortedSigmaField El_Filtration Stochastic_Process Adapted_Stochastic_Process Predictable_Stochastic_Process Set1_of_SigmaField3 Set1_for_RandomVariable Set2_of_SigmaField3 Set2_for_RandomVariable Set3_for_RandomVariable Set4_for_RandomVariable FunctionRV1 FunctionRV2 SetForCall-Option RVProcess -stoch_proc_wrt_to_Filtration Call-Option Convert_REAL is_an_inverseOp_wrt having_an_inverseOp the_inverseOp_wrt Seg 128 FinSequence-like FinSequence len 128 <* *> <*> 254 FinSubsequence-like FinSubsequence Sgm 128 Seq 128 [*] -long FinSequence-membered idseq 128 |-> FinSequenceSet FinSequence-DOMAIN Tuple -tuples_on 128 Del is_one-to-one_at just_once_values <- 100 .. 100 -| 32 |-- 32 -: :- Rev 128 Ins 128 circular Rotate smid ovlpart ovlcon ovlldiff ovlrdiff separates_uniquely is_substring_of is_preposition_of is_postposition_of instr addcr is_terminated_by finite infinite finite-yielding centered "**" 48 findom cup-closed cap-closed diff-closed preBoolean Fin 128 P_1 P_2 P_0 P_A P_e FMT_Space_Str BNbd U_FMT NeighSp Fo_filled ^Fodelta ^Fob ^Foi ^Fos ^Fon ^Fodel_i ^Fodel_o Fo_open Fo_closed ^d Fcl Fint Finf Fdfl are_mutually_symmetric is_continuous Nbdl1 FTSL1 Nbdc1 FTSC1 Nbdl2 FTSL2 Nbds2 FTSS2 is_minimum_path_in inv_continuous U_FMT_filter U_FMT_with_point U_FMT_local U_FMT_filter_base Neighborhood gen_filter FMT_TopSpace TopSpace2FMT FMT2TopSpace FU_FMT gen_top OOpen lim_filtre lim_filtreb U_FT SinglRel FT{0} filled ^delta ^deltai ^deltao ^i ^b ^s ^n ^f ^fb ^fi Lex 255 |^.. +...+ +... *. 250 _ 250 DoubleReorganization valued_reorganization double-one-to-one ^^^ __ >*> <*< .:1 +*1 +*2 +*3 |1 doubleton plus typed/\ /\typed MultPlace AppliedPairwiseTo -multiCat -pr1 -firstChar _\ fixpoints fixpoints1 null typed\ typed| \typed/ -SymbolSubstIn SubstWith SymbolsOf -freeCountableSet -one-to-one -unambiguous -prefix constanT oneone Language string Language-like SubTerms -subTerms -cons -formulasOfMaxDepth AllFormulasOf AllSymbolsOf RelSymbolsOf AtomicTermsOf LettersOf LowerCompoundersOf OwnSymbolsOf TermSymbolsOf OpSymbolsOf Compound -termsOfMaxDepth AllTermsOf AtomicFormulasOf ar TheEqSymbOf TheExSymbOf TheNorSymbOf AtomicFormulaSymbolsOf TrivialArity Depth extendWith addLettersNotIn adicity operational relational literal low-compounding ofAtomicFormula own termal -termal wff 0wff -null eligible -extending Interpreter ExFormulasOf === -ExFunctor ExIterator -NorFunctor NorIterator ReassignIn -placesOf DeTrivial peeler -termEq -TermEval -TruthEval -deltaInterpreter -InterpretersOf -AtomicEval -ExFormulasOf -NorFormulasOf xnot SubWffsOf head tail -interpreter-like -extension -wff exal -nonwff -mincover -absent -occurring -containing -free -covering -satisfying -satisfied -correct -implied AtomicSubst -freeInterpreter Subst1 Subst2 Subst3 Subst4 SubstIn -compound -class -tuple2Class -respecting Rule RuleSet Rule0 Rule1 Rule2 Rule3a Rule3b Rule3c Rule3d Rule3e Rule4 Rule5 Rule6 Rule7 Rule8 Rule9 -diagFormula -provablesFrom -sequents FuncRule AddFormulaTo AddFormulasTo CompletionOf Henkin PairWiseEq -derivables -iterators AddAsWitnessTo AddWitnessesTo WithWitnessesFrom addw -rules OneStep P#0 P#1 P#2 P#3a P#3b P#3c P#3d P#3e P#4 P#5 P#6 P#7 P#8 P#9 R#0 R#1 R#2 R#3a R#3b R#3c R#3d R#3e R#4 R#5 R#6 R#7 R#8 R#9 -sequents-like isotone -ranked -premises-like -inconsistent -inconsistentStrong -consistentWeak -witnessed Correct -macro -provable -consistent -sequent-like -expanded -derivable -mincoverStrong Balls first-countable is_convergent_to Frechet sequential REAL? Cl_Seq disjoint_with_NAT without_zero oper DTConUA FreeOpNSG FreeOpSeqNSG FreeUnivAlgNSG FreeGenSetNSG FreeOpZAO FreeOpSeqZAO FreeUnivAlgZAO FreeGenSetZAO universal_friend with_universal_friend friendship_graph_like Friendship_Graph without_universal_friend BitSubtracterOutput BitSubtracterCirc BorrowIStr BorrowStr BorrowICirc BorrowOutput BorrowCirc BitSubtracterWithBorrowStr BitSubtracterWithBorrowCirc -BitSubtracterStr -BitSubtracterCirc -BitBorrowOutput -BitSubtracterOutput FSM Tran InitS State -succ_of -admissible -leads_to is_admissible_for leads_to_under Mealy-FSM OFun Moore-FSM -response is_similar_to -are_equivalent -equivalent -eq_states_EqR -eq_states_partition final_states_partition -succ_class -class_response the_reduction_of -are_isomorphic reduced accessible accessibleStates -Mealy_union GEN calculating_type is_accessible_via SM_Final FinalS leads_to_final_state_of Moore-SM_Final -TwoStatesMooreSM is_result_of _bool semiautomaton left-Lang automaton right-Lang chop BitFTA0Str BitFTA0Circ BitFTA0CarryOutput BitFTA0AdderOutputI BitFTA0AdderOutputP BitFTA0AdderOutputQ BitFTA1Str BitFTA1Circ BitFTA1CarryOutput BitFTA1AdderOutputI BitFTA1AdderOutputP BitFTA1AdderOutputQ BitFTA2Str BitFTA2Circ BitFTA2CarryOutput BitFTA2AdderOutputI BitFTA2AdderOutputP BitFTA2AdderOutputQ BitFTA3Str BitFTA3Circ BitFTA3CarryOutput BitFTA3AdderOutputI BitFTA3AdderOutputP BitFTA3AdderOutputQ --> 16 [:] 80 [;] 80 Function-yielding .--> IFEQ :-> 128 RealFuncAdd RealFuncMult RealFuncExtMult RealFuncZero RealFuncUnit RealVectSpace RRing Ring AlgebraStr RAlgebra Algebra-like Algebra vector-associative bifunction Covariant Contravariant MSUnTrans BimapStr ObjectMap coreflexive FunctorStr MorphMap Morph-Map id-preserving comp-preserving comp-reversing covariant contravariant injective are_anti-isomorphic idt Function-like Function . 100 one-to-one constant the_value_of functional -compatible quasi_total Funcs 128 onto bijective Permutation /* 128 FUNCTION_DOMAIN chi 128 incl 128 delta 128 +* |: :| +~ curry 128 uncurry 128 curry' 128 uncurry' 128 op0 110 op1 110 op2 110 SubFuncs 128 doms 128 rngs 128 Frege commute In equal_outside compose apply firstdom lastrng FuncSeq-like FuncSequence iter Swap followed_by symmetrical with_symmetrical_domain quasi_even is_even_on quasi_odd is_odd_on signum -periodic periodic f-convex Core strictly-normalized FuzzySet TriangularFS TrapezoidalFS trapezoidal subnormal Membership_Func 1_minus EMF UMF ab_difMF RMembership_Func Zmf Umf converse Imf ext-integer ext-positive ext-negative ExtInt e.i.-valued having_valuation Valuation least-positive normal-valuation 120 Pgenerator NonNegElements ValuatRing PosElements vp scalar-linear multfield diffield "*" NOT1 AND2 OR2 XOR2 EQV2 NAND2 NOR2 AND3 OR3 XOR3 MAJ3 NAND3 NOR3 AND4 OR4 NAND4 NOR4 AND5 OR5 NAND5 NOR5 AND6 OR6 NAND6 NOR6 AND7 OR7 NAND7 NOR7 AND8 OR8 NAND8 NOR8 MODADD2 ADD1 CARR1 ADD2 CARR2 ADD3 CARR3 ADD4 CARR4 MULT210 MULT211 MULT212 MULT213 MULT310 MULT311 MULT312 MULT313 MULT314 MULT321 MULT322 MULT323 MULT324 CLAADD1 CLACARR1 CLAADD2 CLACARR2 CLAADD3 CLACARR3 CLAADD4 CLACARR4 G_RAT G_INTEG g_rat_add g_rat_mult RSc_Mult F_Rat Gauss_RAT_Module Gauss_RAT_Ring Gauss_RAT_Field g_int_unit g_prime g_rational G_RAT_SET g_int_add g_int_mult Gauss_INT_Field Gauss_INT_Module Gauss_INT_Ring Z_AlgebraStr Z_Algebra Sc_Mult g_integer G_INT_SET Divides is_associated_to is_not_associated_to Classes Am AmpleSet NF gcd-like gcdDomain are_canonical_wrt are_co-prime are_normalized_wrt add1 add2 mult1 mult2 Gene-Set GA-Space Individual crossover are_DTr_wrt DTrapezium MidPoint AfMidStruct DTrSpace MidOrdTrapSpace-like MidOrdTrapSpace OrdTrapSpace-like OrdTrapSpace TrapSpace-like TrapSpace Regular inv1 buf1 and2c xor2c GFA0CarryIStr GFA0CarryICirc GFA0CarryStr GFA0CarryCirc GFA0CarryOutput GFA0AdderStr GFA0AdderCirc GFA0AdderOutput BitGFA0Str BitGFA0Circ BitGFA0CarryOutput BitGFA0AdderOutput GFA1CarryIStr GFA1CarryICirc GFA1CarryStr GFA1CarryCirc GFA1CarryOutput GFA1AdderStr GFA1AdderCirc GFA1AdderOutput BitGFA1Str BitGFA1Circ BitGFA1CarryOutput BitGFA1AdderOutput GFA2CarryIStr GFA2CarryICirc GFA2CarryStr GFA2CarryCirc GFA2CarryOutput GFA2AdderStr GFA2AdderCirc GFA2AdderOutput BitGFA2Str BitGFA2Circ BitGFA2CarryOutput BitGFA2AdderOutput GFA3CarryIStr GFA3CarryICirc GFA3CarryStr GFA3CarryCirc GFA3CarryOutput GFA3AdderStr GFA3AdderCirc GFA3AdderOutput BitGFA3Str BitGFA3Circ BitGFA3CarryOutput BitGFA3AdderOutput -BitGFA0Str -BitGFA0Circ -BitGFA0CarryOutput -BitGFA0AdderOutput -BitGFA1Str -BitGFA1Circ -BitGFA1CarryOutput -BitGFA1AdderOutput GraphStruct VertexSelector EdgeSelector SourceSelector TargetSelector _GraphSelectors the_Vertices_of the_Edges_of the_Source_of the_Target_of [Graph-like] _Graph createGraph .set 160 .strict Joins DJoins SJoins DSJoins loopless non-multi non-Dmulti simple Dsimple .order() 160 .size() 160 .edgesInto 160 .edgesOutOf 160 .edgesInOut 160 .edgesBetween 160 .edgesDBetween 160 Subgraph spanning == != inducedSubgraph removeVertex removeVertices removeEdge removeEdges Vertex .edgesIn() 160 .edgesOut() 160 .edgesInOut() 160 .adj 160 .inDegree() 160 .outDegree() 160 .degree() 160 .inNeighbors() 160 .outNeighbors() 160 .allNeighbors() 160 isolated endvertex Graph-yielding halting .Lifespan() 160 .Result() 160 GraphSeq non-trivial VertexSeq EdgeSeq Walk .walkOf 160 .first() 160 .last() 160 .vertexAt 160 .reverse() 160 .append 160 .cut 160 .remove 160 .addEdge 160 .vertexSeq() 160 .edgeSeq() 160 .vertices() 160 .edges() 160 .length() 160 .find 160 .rfind 160 is_Walk_from Trail-like Path-like vertex-distinct Cycle-like Trail DWalk DTrail DPath Subwalk .allWalks() 160 .allTrails() 160 .allPaths() 160 .allDWalks() 160 .allDTrails() 160 .allDPaths() 160 acyclic is_DTree_rooted_at .reachableFrom 160 .reachableDFrom 160 Component-like .componentSet() 160 .numComponents() 160 cut-vertex WeightSelector ELabelSelector VLabelSelector [Weighted] [ELabeled] [VLabeled] WGraph EGraph VGraph WEGraph WVGraph EVGraph WEVGraph the_Weight_of the_ELabel_of the_VLabel_of weight-inheriting elabel-inheriting vlabel-inheriting WSubgraph ESubgraph VSubgraph WESubgraph WVSubgraph EVSubgraph WEVSubgraph inducedWSubgraph inducedESubgraph inducedVSubgraph inducedWESubgraph inducedWVSubgraph inducedEVSubgraph inducedWEVSubgraph real-weighted nonnegative-weighted real-elabeled real-vlabeled real-WEV .weightSeq() 160 .cost() 160 .labeledE() 160 .labelEdge 160 .labelVertex 160 .labeledV() 160 WGraphSeq EGraphSeq VGraphSeq WEGraphSeq WVGraphSeq EVGraphSeq WEVGraphSeq is_mincost_DTree_rooted_at is_mincost_DPath_from .min_DPath_cost 160 WGraphSelectors .allWSubgraphs() 160 DIJK:Labeling DIJK:NextBestEdges 160 DIJK:Step 160 DIJK:Init 160 DIJK:LabelingSeq DIJK:CompSeq 160 DIJK:SSSP 160 PRIM:Labeling PRIM:NextBestEdges 160 PRIM:Init 160 PRIM:Step 160 PRIM:LabelingSeq PRIM:CompSeq 160 PRIM:MST 160 min-cost minimumSpanningTree natural-weighted FF:ELabeling has_valid_flow_from .flow 160 has_maximum_flow_from AP:VLabeling is_forward_edge_wrt is_backward_edge_wrt is_augmenting_wrt AP:NextBestEdges 160 AP:Step 160 AP:VLabelingSeq AP:CompSeq 160 AP:FindAugPath 160 AP:GetAugPath 160 .flowSeq .tolerance FF:PushFlow FF:Step FF:ELabelingSeq FF:CompSeq FF:MaxFlow X_axis 255 Y_axis 255 X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column Go-board is_sequence_on GoB 128 Incr 128 lies_between v_strip h_strip cell s.c.c. standard special_circular_sequence right_cell left_cell LeftComp RightComp aren't_adjacent Values front_right_cell front_left_cell turns_right turns_left goes_straight satisfiable free_symbol FCEx Example_of Example_Formula_of Example_Formulae_of FCEx-Sequence -th_FCEx EF-Sequence -th_EF negation_faithful with_examples ExCl Ex-bound_in Ex-the_scope_of := repeat OuterVx LifeSpan while_do XEdge Weight UnusedVx UsedVx Argmin findmin newpathcost hasBetterPathAt Relax equal_at is_vertex_seq_at is_simple_vertex_seq_at is_oriented_edge_seq_of is_Input_of_Dijkstra_Alg DijkstraAlgorithm MultiGraphStruct Source Target Edge Graph cod 128 is_sum_of oriented joins are_incident Path OrientedPath cyclic Cycle OrientedCycle VerticesCount EdgesCount EdgesIn EdgesOut Degree -cut ^' TwoValued Alternating -VSet is_vertex_seq_of alternates_vertices_in vertex-seq min_at is_non_decreasing_on is_split_at Edges_In Edges_Out Edges_At AddNewEdge -CycleSet CatCycles -PathSet ExtendCycle Eulerian KVertices KEdges KSource KTarget KoenigsbergBridges orientedly_joins are_orientedly_incident -SVSet -TVSet is_oriented_vertex_seq_of oriented-vertex-seq Simple vertices is_orientedpath_of OrientedPaths is_acyclicpath_of AcyclicPaths Real>=0 is_weight>=0of is_weight_of RealSequence cost is_shortestpath_of islongestInShortestpath Morphs cat ZeroMap GroupMorphismStr Fun fun ZERO 128 GroupMorphism-like GroupMorphism Group_DOMAIN-like Group_DOMAIN GroupMorphism_DOMAIN-like GroupMorphism_DOMAIN MapsSet GO GroupObjects GroupCat AbGroupObjects AbGroupCat MidOpGroupObjects MidOpGroupCat the_normal_subgroups_of multiples is_Groebner_basis_wrt is_Groebner_basis_of DivOrder is_monic_wrt is_reduced_wrt is_autoreduced_wrt are_disjoint are_non_disjoint S-Poly is_MonomialRepresentation_of is_Standard_Representation_of has_a_Standard_Representation_of Upper_Support Lower_Support Low expon -power -commutative-group -commutative-group-like unital Group-like Group 1_ inverse_op 124 power 124 being_of_order_0 ord 128 unity-preserving being_left_operation LeftOperation the_left_translation_of the_left_operation_of the_subsets_of_card the_extension_of_left_translation_of the_extension_of_left_operation_of the_strict_stabilizer_of is_fixed_under the_fixed_points_of are_conjugated_under the_orbit_of the_orbits_of is_p-group_of_prime is_Sylow_p-subgroup_of_prime the_sylow_p-subgroups_of_prime -group ProjSet ProjGroup 1ProdHom Z/Z Ordset Group-Family ProductMap SumMap DirectSumComponents mult 124 add_inverse 124 addGroup addGroup-like zero-preserving TopaddGrStr TopaddGroup TopologicaladdGroup add-unital Subgroup (1). 128 carr 128 Left_Cosets 128 Right_Cosets 128 Index 128 Subgroup-Family component-commutative trans_prod trans_sum prod_bundle sum_bundle dprod dsum dprod2prod prod2dprod supp_restr dsum2sum sum2dsum InterHom ProductHom Subgroups 124 are_conjugated are_not_conjugated con_class 124 Normalizer 123 gr 124 maximal Phi 124 lattice 124 commutators 124 center 124 Cosets 148 CosOp 148 ./. 100 Homomorphism 1: 148 nat_hom 148 Ker 148 Image 148 multMagma-yielding multMagma-Family Double_Cosets Action is_stable_under_the_action_of the_stable_subset_generated_by HGrWOpStr action GroupWithOperators StableSubgroup the_stable_subgroups_of CosAc homomorphic the_stable_subgroup_of composition_series CompositionSeries strictly_decreasing jordan_holder the_series_of_quotients_of are_equivalent_under the_schreier_series_of solvable GRZ-ops GRZ-symbols GRZ-op-arity GRZ-arity GRZ-formula-set GRZ-formula GRZ-axioms GRZ-axiomatic GRZ-rule GRZ-MP GRZ-ConjIntro GRZ-ConjElimL GRZ-ConjElimR GRZ-rules GRZ-formula-sequence GRZ-formula-finset GRZ-provable LD-specific-axioms LD-axioms LD-axiomatic LD-provable LD-= LD-EqR LD-EqClasses LD-EqClass LD-EqClassOf INT.Group @' Safe Sophie_Germain Mersenne TarskiPlane Betweenness Equidistance between equiv cong satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity satisfying_Pasch satisfying_Tarski-model are_ordered Collinear on_line equal_line TarskiExtension MetrTarskiStr TarskiSpace Tarski0Space is_Between close-everywhere TrivialTarskiSpace TarskiEuclid2Space TarskiEuclidSpace satisfying_A8 satisfying_A9 satisfying_A10 satisfying_A11 satisfying_Lower_Dimension_Axiom satisfying_Upper_Dimension_Axiom satisfying_Euclid_Axiom satisfying_Continuity_Axiom Functional subadditive positively_homogeneous semi-homogeneous absolutely_homogeneous 0-preserving Banach-Functional linear-Functional [** **] i_FC 0Functional RFunctional Real_homogeneous 0RFunctional Semi-Norm RealVS projRe projIm RtoC CtoR i-shift prodReIm Cut is_a_system_of_different_representatives_of Hall Reduction Singlification HausDist maxPrefix _Tree _Subtree .pathBetween 96 MiddleVertex with_Helly_property Consistent Inconsistent HCar Henkin_interpretation valH cmplxhomogeneous antilinear-Functional QcFunctional cmplxhomogeneousFAF hermitan diagRvalued diagReR+0valued sesquilinear-Form hermitan-Form signnorm quasinorm RQ*Form Q*Form positivediagvalued ScalarForm Atom 110 pair_diff 110 =>> 30 pseudo_compl 110 StrongImpl 110 SUB 110 Involved SubstPoset PFArt PFCrt PFBrt PFDrt object <> in strict bag_extend UnitBag 1_1 minlen monomial upm mpu with_VERUM with_implication with_conjunction with_propositional_variables HP-closed HP-WFF HP-formula Hilbert_theory CnPos HP_TAUT prop HP-Subformulae SetValuation SetVal Perm canonical pseudo-canonical SetValuation0 ChoiceOn FieldCover SetVal0 SomePoints OtherPoints tohilb tohilbperm tohilbval classical is_Sc is_constructingBinHuffmanTree Initial-Trees IndexedREAL MakeTree Vtree Vrootr Vrootl MaxVl BinFinTrees BoolBinFinTrees LeavesSet BinHuffmanTree MinValueTree Coeff deg rpoly qpoly Hurwitz F* even_part odd_part with_all_coefficients with_positive_coefficients with_negative_coefficients one_port_function reactance_one_port_function add-closed left-ideal right-ideal RightIdeal LeftIdeal add| mult| Gr LinearCombination LeftLinearCombination RightLinearCombination -Ideal -LeftIdeal -RightIdeal finitely_generated Noetherian PID is_expressible_by ADD_MOD 128 NEG_N 128 NEG_MOD 128 ChangeVal_1 128 ChangeVal_2 128 MUL_MOD 128 INV_MOD 128 IDEAoperationA 128 IDEAoperationB 128 IDEAoperationC 128 MESSAGES 128 IDEA_P 128 IDEA_Q 128 IDEA_P_F 128 IDEA_Q_F 128 IDEA_PS 128 IDEA_QS 128 IDEA_PE 128 IDEA_QE 128 ProjectiveLines Proj_Inc IncProjSp_of partial up-2-dimensional up-3-rank IncProjSp 3-dimensional IncProjStr Points Lines Inc IncStruct Planes Inc2 Inc3 POINT LINE PLANE on planar with_non-trivial_lines up-2-rank with_non-empty_planes with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible IncSpace-like IncSpace Line 15 Plane 15 Category-yielding ManySortedCategory Objs Mphs Category-yielding_on_first Function-yielding_on_second ManySortedFunctor Indexing TargetCat coIndexing -functor -indexing_of Subsignature is_right_ext_Riemann_integrable_on is_left_ext_Riemann_integrable_on ext_right_integral ext_left_integral is_+infty_ext_Riemann_integrable_on is_-infty_ext_Riemann_integrable_on infty_ext_right_integral infty_ext_left_integral infty_ext_Riemann_integrable infty_ext_integral exp*- One-sided_Laplace_transform middle_volume middle_sum middle_volume_Sequence R2-to-C C1-curve-like C1-curve xvol vvol var_volume vd total_vd bounded_variation is_RiemannStieltjes_integrable_with closed-interval Division divs divset upper_volume lower_volume upper_sum lower_sum upper_sum_set lower_sum_set upper_integrable lower_integrable upper_integral lower_integral integrable integral indx PartSums DivSequence divide_into_equal is_integrable_on [' '] IntegralFuncs is_integral_of Cst |||( )||| is_orthogonal_with ||.. ..|| Inter IntervalSet _/\_ _\/_ ``2 80 ordered _\_ IntervalSets InterLatt RS RoughSets RSLattice ERS with_FALSUM with_int_implication with_int_conjunction with_int_disjunction with_int_propositional_variables with_modal_operator MC-closed MC-wff MC-formula Nes IPC_theory CnIPC IPC-Taut neg IVERUM CPC_theory CnCPC CPC-Taut S4_theory CnS4 S4-Taut integer Integer are_congruent_mod [\ /] [/ \] frac 140 div 32 mod 32 dim-like gcd 32 prime INT.Ring absint Euclidian EuclidianRing DegreeFunction Cong is_CRS_of Poly-INT is_quadratic_residue_mod Lege multiplicative-trivial Chinese_Remainder CR_Sequence CR_coefficients to_int prime-factorization-like Segm0 multint0 Z/Z* RelPrimes is_primitive_root_of is_RRS_of irrational aseq 250 bseq 250 cseq 250 dseq 250 eseq 250 is_equivalent_with Equivalence export distribute supercondensed subcondensed regular_open regular_closed Bound Border are_c=-incomparable 1st_class 2nd_class 3rd_class with_1st_class_subsets with_2nd_class_subsets with_3rd_class_subsets PGraph PairF is_Shortcut_of nodic Out_In_Sq AffineMap Sq_Circ NormF 101 FanW -FanMorphW 101 FanN -FanMorphN 101 FanE -FanMorphE 101 FanS -FanMorphS 101 rectangle inside_of_rectangle closed_inside_of_rectangle outside_of_rectangle closed_outside_of_rectangle circle inside_of_circle closed_inside_of_circle outside_of_circle closed_outside_of_circle diffX2_1 diffX2_2 diffX1_X2_1 diffX1_X2_2 Proj2_1 Proj2_2 DiskProj RotateCircle Jordan UBD-Family BDD-Family ApproxIndex Y-InitStart Y-SpanStart is_in_general_position_wrt are_in_general_position Span SpanStart are_in_this_order_on North-Bound South-Bound -separate are_neighbours_wrt Upper_Appr Lower_Appr North_Arc South_Arc Center Upper_Seq Lower_Seq RealOrd X-SpanStart is_sufficiently_large_for is_Lin is_Rin is_Lout is_Rout is_OSin is_OSout with_the_max_arc UMP LMP almost-one-to-one weakly-one-to-one poorly-one-to-one realize-max-dist-in Bounded is_inside_component_of is_outside_component_of BDD UBD 1* 1.REAL mid is_S-Seq_joining L_Cut R_Cut LE LT B_Cut S_Drop is_a_part>_of is_a_part<_of is_a_part_of Lower Upper First_Point Last_Point i_s_w i_n_w i_s_e i_n_e i_w_s i_e_s i_w_n i_e_n n_s_w n_n_w n_s_e n_n_e n_w_s n_e_s n_w_n n_e_n x_Middle y_Middle L_Segment R_Segment Segment Vertical_Line Horizontal_Line Upper_Arc Lower_Arc Lower_Middle_Point Upper_Middle_Point Gauge Cage Eucl_dist Segmentation S-Gap lfp gfp +. -. FixPoints Indep ManySortedSigmaField is_independent_wrt SigmaSection sigUn futSigmaFields tailSigmaField MeetSections finSigmaFields Kurat14Part Kurat14Set Kurat14ClPart Kurat14OpPart Kurat7Set KurExSet Cl-closed Int-closed Lim_K Lim_inf Lim_sup MODMAP_ LAG4SQf LAG4SQg a_sum_of_four_squares DTConstrStr Rules GrammarStr InitialSym Symbol String Terminals NonTerminals is_derivable_from Lang EmptyGrammar SingleGrammar IterGrammar TotalGrammar effective Delete ReplaceCol RCol Rem Minor Cofactor Matrix_of_Cofactor LaplaceExpL LaplaceExpC Stone pseudocomplemented is_a_pseudocomplement_of Skeleton satisfying_Stone_identity SkelLatt DenseElements DenseLatt squared squared-latt skeletal Distributive Meet-absorbing Meet-Absorbing AD_Lattice /\-Associative left-Distributive GAD_Lattice lub glb ex_lub_of ex_glb_of bottom ADL-absorbing LatOrder LatRelStr ThetaOrder SubLattStr example32"/\" example32"\/" example32/\ example32\/ example33"/\" example33"\/" example33/\ example33\/ absorbs doesn't_absorb FinJoin 150 FinMeet 150 D0_Lattice Heyting H_Lattice BooleLatt LattPOSet % 200 is_<=_than is_>=_than with_suprema with_infima is_less_than is_greater_than \/-distributive /\-distributive preserves_implication preserves_top preserves_bottom preserves_complement ClosedSubset field_by SetImp EqRelLATT Sublattice are_joint_by type_of BiFunction u.t.i. distance_function alpha new_set new_bi_fun DistEsti ConsecutiveSet QuadrSeq Quadr BiFun ConsecutiveDelta NextSet NextDelta is_extension_of ExtensionSeq BasicDF noetherian co-noetherian is-upper-neighbour-of is-lower-neighbour-of completely-meet-irreducible completely-join-irreducible co-atomic supremum-dense infimum-dense MIRRS JIRRS <(1) Join-IRR LOWER Ring_of_sets finitely_typed has_a_representation_of_type<= new_set2 new_bi_fun2 ConsecutiveSet2 Quadr2 ConsecutiveDelta2 NextSet2 NextDelta2 is_extension2_of ExtensionSeq2 PrimeFilters 200 PseudoComplements Spectrum PseudoCocomplements unordered PFilters /\-SemiLattStr L_meet \/-SemiLattStr L_join LattStr "/\" join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like Lattice distributive modular lower-bounded upper-bounded D_Lattice M_Lattice 0_Lattice 1_Lattice 01_Lattice Bottom 129 Top 129 is_a_complement_of complemented C_Lattice Boolean B_Lattice final meet-closed join-closed with_finite-elements .\/ natsubset-yielding .incSubset iterative eventually-constant preVNumberingSeq vertex-numbering VNumberingSeq .PickedAt LexBFS:Labeling LexBFS:Init LexBFS:PickUnnumbered LexBFS:Update LexBFS:Step LexBFS:LabelingSeq ``1 LexBFS:CSeq with_property_L3 MCS:Labeling MCS:Init MCS:PickUnnumbered MCS:LabelAdjacent MCS:Update MCS:Step MCS:LabelingSeq MCS:CSeq with_property_T RealPoset <<= >>= ~<= ~>= FuzzyLattice TrCl left_open_halfline left_closed_halfline right_closed_halfline right_open_halfline divergent_to+infty divergent_to-infty convergent_in+infty divergent_in+infty_to+infty divergent_in+infty_to-infty convergent_in-infty divergent_in-infty_to+infty divergent_in-infty_to-infty lim_in+infty lim_in-infty is_left_convergent_in is_left_divergent_to+infty_in is_left_divergent_to-infty_in is_right_convergent_in is_right_divergent_to+infty_in is_right_divergent_to-infty_in lim_left lim_right is_convergent_in is_divergent_to+infty_in is_divergent_to-infty_in SUBMODULE_DOMAIN LINE_DOMAIN lines HIPERPLANE HIPERPLANE_DOMAIN hiperplanes COMPL ADD LMULT FuncAdd FuncExtMult FuncZero LinearOperator LinearOperators R_VectorSpace_of_LinearOperators BoundedLinearOperators R_VectorSpace_of_BoundedLinearOperators modetrans PreNorms BoundedLinearOperatorsNorm R_NormSpace_of_BoundedLinearOperators RealBanachSpace FuncMult FuncUnit Ring_of_BoundedLinearOperators R_Algebra_of_BoundedLinearOperators BLAlgebra Normed_AlgebraStr R_Normed_Algebra_of_BoundedLinearOperators Normed_Algebra Banach_Algebra-like_1 Banach_Algebra-like_2 Banach_Algebra-like_3 Banach_Algebra-like Banach_Algebra norm_summable are_commutative exp_ graphNrm graphNSP OpenClosedSet T_join T_meet OpenClosedSetLatt ultraset UFilter 200 StoneR StoneSpace StoneBLattice multcpfunc multcomplexcpfunc CPFuncZero CPFuncUnit addcpfunc CLSp_PFunct L1_CFunctions CLSp_L1Funct AlmostZeroCFunctions CLSp_AlmostZeroFunct a.e-Ceq-class CCosetSet addCCoset zeroCCoset lmultCCoset Pre-L-CSpace L-1-CSpace L-1-CNorm a.e.cpfunc= multi-closed multpfunc multrealpfunc RealPFuncZero RealPFuncUnit RLSp_PFunct L1_Functions RLSp_L1Funct a.e.= AlmostZeroFunctions RLSp_AlmostZeroFunct a.e-eq-class Pre-L-Space L-1-Norm L-1-Space Lp_Functions RLSp_LpFunct AlmostZeroLpFunctions RLSp_AlmostZeroLpFunct a.e-eq-class_Lp Pre-Lp-Space Lp-Norm Lp-Space geq_than_1 rto_power the_set_of_RealSequences_l^ l_norm^ l_Space^ LTLB_WFF TFALSUM TVERUM '&&' 'G' 'F' 'Uw' with_LTL_axioms LTL_axioms MP_rule NEX_rule IND_rule prc LTL_TAUT_OF_PL props SAT axltl1 axltl1a axltl2 axltl3 axltl4 axltl5 axltl6 untn con impg nega nex ctaut PNPair tau1 without_implication pnptree Subt compl is_completion_of compn rngr s-until rarg |=0 with_LTL0_axioms LTL0_axioms MP0_rule REFL0_rule NEX0_rule IND0_rule prc0 |-0 implications relation the_arity_of 20 relation_length relations_on empty_rel BOOLEAN ALL boolean-valued (+) 32 (O) 40 (o) 40 (.) (&) (@) Positive Negative Nonpositive Nonnegative is_less_or_equal_with 2Set Part_sgn ReplaceLine RLine addFinS InterchangeLine ScalarXLine RlineXScalar ILine SXLine RLineXS InterchangeCol ScalarXCol RcolXScalar ICol SXCol RColXS EqSegm without_repeated_line FinS2MX MX2FinS SwapDiagonal Solutions_of Space_of_Solutions_of is_line_circulant_about line_circulant first-line-of-circulant is_col_circulant_about col_circulant first-col-of-circulant LCirc CCirc circulant is_anti-circular_about anti-circular first-line-of-anti-circular ACirc subsymmetric Anti-subsymmetric central_symmetric is_symmetry_circulant_about symmetry_circulant first-symmetry-of-circulant SCirc @" FinSeq2Matrix Matrix2FinSeq FR2FC LineSum ColSum SumAll QuadraticForm Matrix-yielding FinSequence_of_Matrix Len Width block_diagonal Square-Matrix-yielding FinSequence_of_Square-Matrix Jordan_block Jordan-block-yielding FinSequence_of_Jordan_block degree_of_nilpotent MXR2MXF MXF2MXR 0_Rmatrix ColVec2Mx LineVec2Mx 1_Rmatrix Base_FinSeq -size tabular Matrix Indices Col -Matrices_over diagonal Diagonal -G_Matrix_over ][ 100 upper_triangular lower_triangular DelCol DelLine Deleting permutational Permutations Group_of_Perm being_transposition FinOmega Path_matrix Path_product Det diagonal_of_Matrix COMPLEX2Field Field2COMPLEX 0_Cx is_reverse_of Orthogonal IFIN Idempotent Nilpotent Involutory Self_Reversible is_congruent_Matrix_of PPath_product OrdBasis lmlt AutMt AutEqMt Mx2Tran c/= SubsetFamilyStr dependent the_family_of with_exchange_property Matroid finite-membered finite-degree ProdMatroid LinearlyIndependentSubsets is_maximal_independent_in Rnk is_dependent_on cycle ProbFinS m-nonnegative with_sum=1 Joint_Probability with_line_sum=1 Conditional_Probability Row_Marginal Column_Marginal rotation base_rotation -support-yielding Rotation AxialSymmetry midpoints-preserving -reflection `1 255 `2 255 `3 255 `4 255 pr1 128 pr2 128 `11 255 `12 255 `21 255 `22 255 `5 255 `6 255 `7 255 `8 255 `9 255 Family_of_Intervals product-pre-Measure SemialgebraFamily FieldFamily MeasureFamily measurable_rectangles Xchi Measure measure_zero N_Sub_set_fam sigma-additive Sep_Sequence sigma_Measure N_Measure_fam N_Sub_fam is_complete thin COM MeasPart C_Measure sigma_Field sigma_Meas open_interval closed_interval right_open_interval left_closed_interval left_open_interval right_closed_interval interval Interval diameter R_EAL Interval_Covering vol Svc OS_Meas Lmi_sigmaFIELD L_mi Sep_FinSequence Set_Sequence Covering Volume C_Meas InvPairFunc completely-additive Length joined_FinSeq joined_seq pre-Measure additive-like induced_Measure induced_sigma_Measure complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered -- 32 "" ++ 32 ** /// Trivial-Mem Mem-Struct Location LocationsF ValuesF the_Values_of with_non-empty_values uniformly_bounded is_uniformly_convergent_to INT- RAT_with_denominator 1. eq_dom less_dom less_eq_dom great_dom great_eq_dom is_measurable_on Finite_Sep_Sequence is_simple_func_in are_Re-presentation_of nonpositive without-infty without+infty ExtREAL_sequence convergent_to_finite_number convergent_to_+infty convergent_to_-infty integral' integral+ Integral Integral_on extreal-yielding multextreal with_the_same_dom ProjMap1 ProjMap2 MetrStruct distance dist Empty^2-to-zero Reflexive discerning triangle MetrSpace discrete_dist DiscreteSpace real_dist RealSpace Ball cl_Ball Sphere PseudoMetricSpace Discerning SemiMetricSpace NonSymmetricMetricSpace ultra UltraMetricSpace Set_to_zero ZeroSpace is_between open_dist_Segment close_dist_Segment -neighbour equivalence_class is_dst ev_eq_1 ev_eq_2 real_in_rel elem_in_rel_1 elem_in_rel_2 elem_in_rel set_in_rel nbourdist Eq_classMetricSpace dist_cart2 dist2 MetrSpaceCart2 dist_cart3 MetrSpaceCart3 dist3 dist_cart4 MetrSpaceCart4 dist4 dist_cart2S dist2S MetrSpaceCart2S dist_cart3S dist3S MetrSpaceCart3S taxi_dist2 RealSpaceCart2 Eukl_dist2 EuklSpace2 taxi_dist3 RealSpaceCart3 Eukl_dist3 EuklSpace3 bounded_metric is_convergent_in_metrspace_to contains_almost_all_sequence dist_to_point sequence_of_dist Lindelof separates with_boundary without_boundary locally_euclidean topological_manifold -dimensional manifold Tball Tunit_ball ball manifold-like -locally_euclidean -manifold TUnitSphere TPlane stereographic_projection InnerProduct MidStr MIDPOINT Example 16 MidSp-like MidSp @@ ## ID 128 vect 32 setvect addvect complvect zerovect vectgroup is_atlas_of midpoint_operator Half Atlas MidSp. AtlasStr algebra function ATLAS-like ATLAS associating ReperAlgebraStr reper being_invariance has_property_of_zero_in is_semi_additive_in is_additive_in is_alternative_in ReperAlgebra \, beta-transitive number_of value_of first resource iteration_of List Operation \& WHERE WHEREeq WHERElt WHEREle WHEREgt WHEREge AND OR BUTNOT NOT filtering #occurrences max# ROUGH ATLEAST ATMOST EXACTLY ATLEAST- ATMOST+ EXACTLY+- ref-finite ConstructorDB Constrs ref-operation ref occur Root MP-variables MP-variable MP-conectives MP-conective DOMAIN_DecoratedTree MP-WFF MP-wff ? necessitive LeftMod_DOMAIN LModMorphism_DOMAIN LModObjects dom' cod' LModCat k_id k_nat UnivF Castboolean CastBool atom. EX EG EU CTL_WFF CTL-formula-like CTL-formula ExistNext ExistGlobal ExistUntill CastCTLformula KripkeStr Worlds Starts Possibles Label CTLModelStr Assignations BasicAssign And Not EneXt EGlobal EUntill Assign atomic_WFF is-Evaluation-for is-PreEvaluation-for GraftEval EvalSet CastEval EvalFamily Evaluate |** inf_path ModelSP Fid Not_0 Not_ EneXt_univ EneXt_0 EneXt_ EGlobal_univ EGlobal_0 EGlobal_ And_0 And_ EUntill_univ EUntill_0 EUntill_ F_LABEL Label_ KModel BASSModel |/= PrePath Pred SIGMA Tau Fax SigFaxTau PathShift PathChange PathConc TransEG Foax SigFoaxTau TransEU with_basic CTLModel TrivialCTLModel CastNat 'X' 'U' 'R' LTL_WFF LTL-formula-like LTL-formula next Until Release CastLTL LTLModelStr Or NEXT UNTIL RELEASE atomic_LTL Inf_seq CastSeq Next_univ Next_0 Next_ Until_univ Until_0 Until_ Or_ Release_ Inf_seqModel AtomicFamily AtomicFunc AtomicAsgn AtomicBasicAsgn AtomicKai LTLModel TrivialLTLModel LTLNew1 LTLNew2 LTLNext LTLnode LTLold LTLnew LTLnext SuccNode1 SuccNode2 is_succ_of is_succ1_of is_succ2_of failure elementary Seed FinalNode CastNode is_Finseq_for is_next_of Length_fun Partial_seq LTLNodes LTLStates is_succ_homomorphism chosen_formula chosen_succ choice_succ_func neg-inner-most BuchiAutomaton is-accepted-by Neg_atomic_LTL Tran_LTL InitS_LTL FinalS_LTL BAutomaton chosen_succ_end_num chosen_next chosen_run TrivialLMod LModMorphismStr Dom Cod LModMorphism-like LModMorphism add3 mult3 compl3 unit3 zero3 Z_3 base antimultiplicative antilinear monomorphism antimonomorphism epimorphism antiepimorphism isomorphism antiisomorphism endomorphism antiendomorphism automorphism antiautomorphism Endomorphism Automorphism square-containing square-free SCNAT Moebius 128 NatDivisors SMoebius 128 PFactors Radical Divisors_Lattice ReciPrime divergent SqFactors SqF TSqFactors TSqF invNAT BoolePrime constituted-Functions constituted-FinSeqs (*) 128 left-invertible right-invertible left-cancelable right-cancelable uniquely-decomposable Monoid MonoidalExtension SubStr MonoidalSubStr *+^ *+^+<0> -concatenation GPFuncs MPFuncs -composition GFuncs MFuncs GPerms MultiSet_over Multiset finite-MultiSet_over .:^2 230 binary-image dilation erosion binary-image-family coprod GeneratorSet REL DTConMSA Sym 255 FreeSort DenOp FreeOper FreeMSA FreeGen Reverse Flatten SingleAlg SortsWithConstants InputVertices InnerVertices with_input_V InputValues Circuit-like action_at FreeEnv Eval finitely-generated monotonic depth -terms image -Image canonical_homomorphism terminating NFAlgebra NForms NF-var all_vars_including inheriting_operations free_in_itself struct-invariant -different sufficiently_rich growable -ary_oper_including -sort construction_degree deg<= height<= -context -omitting context -dependent -context_including -context_in -context_pos_in -sub -constant -reachable -sorts -context-sequence vf-sequence -consequent-context-sequence infinite-yielding OrderedAlgFam Binding bind normalized Normalized InvLim MSS-membered TrivialMSSign MSS_set MSS_morph -Terms Term ArgumentSeq c-Term -term CompoundTerm SetWithCompoundTerm Variables is_an_evaluation_of MSSCat MSAlg_set MSAlg_morph MSAlgCat directed_cycle-less with_directed_cycle well-founded finitely_operated InducedEdges InducedSource InducedTarget InducedGraph MSSubsetFamily additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound ManySortedSign Arity ResultSort SortSymbol OperSymbol the_result_sort_of many-sorted Sorts MSAlgebra Charact Args Result Den segmental MSSign MSSorts MSCharact MSAlg the_sort_of the_charact_of 1-Alg MSSubset all-with_const_op MSSubAlgebra SubSort MSSubSort GenMSAlg MSSub MSAlg_join MSAlg_meet MSSubAlLattice "1-1" "onto" is_homomorphism is_epimorphism is_monomorphism is_isomorphism Relation-yielding ManySortedRelation MSEquivalence_Relation-like MSEquivalence-like MSCongruence-like MSCongruence QuotRes QuotArgs QuotCharact QuotMSAlg MSNat_Hom MSCng MSHomQuot EqCl EqRelLatt CongrLatt feasible TranslationRel is_e.translation_of Translation compatible invariant InvCl StabCl TRS EquationalTheory EqTh /\-inheriting \/-inheriting RealSubLatt CongrCl EqRelSet Mpr1 Mpr2 Over TriOp QuaOp with_finite_chromatic# chromatic# with_finite_cliquecover# cliquecover# Adjacent NatRelStr CompleteRelStr Mycielskian FamilySequence sigma_discrete sigma_locally_finite uncountable Basis_sigma_discrete Basis_sigma_locally_finite is_a_pseudometric_of PairFunc transformation `*` 120 is_naturally_transformable_to natural_transformation are_naturally_equivalent ~= natural_equivalence NatTrans-DOMAIN NatTrans Functors discrete IdCat Nat min* sequence ^\ |-count prime_exponents 60 pfexp 60 prime_factorization 60 ppf 60 EXP Euler_phi _greater _or_smaller _smaller Divisor PrimeDivisor Proth FermatNumber Ferm CullenNumber Cullen is_quadratic_non_residue_mod LegendreSymbol Leg hcflat lcmlat Nat_Lattice 0_NN 1_NN NATPLUS NatPlus hcflatplus lcmlatplus NatPlus_Lattice SubLattice XORB ZeroB -BinaryGroup MLTB -BinaryVectSp is_Gateaux_differentiable_in Gateaux_diff diff_SP IsoCPNrSP IsoPCNrSP reproj1 reproj2 is_partial_differentiable_in`1 is_partial_differentiable_in`2 partdiff`1 partdiff`2 is_partial_differentiable_on`1 is_partial_differentiable_on`2 `partial`1| `partial`2| embeds is_equimorphic_to parallel -SuccRelStr SymRelStr ComplRelStr Necklace N-free union_of sum_of fin_RelStr fin_RelStr_sp path path-connected component NelsonStr Nnegation impl Iimpl unity satisfying_A1 satisfying_A1b satisfying_A2 satisfying_N3 satisfying_N4 satisfying_N5 satisfying_N6 satisfying_N7 satisfying_N8 satisfying_N9 satisfying_N10 satisfying_N11 satisfying_N12 satisfying_N13 Nelson_Algebra DeMorgan_Algebra DeMorgan Quasi-Boolean_Algebra =-> satisfying_N0* satisfying_N1* satisfying_N2* satisfying_N3* satisfying_N4* satisfying_N5* satisfying_N6* satisfying_N7* satisfying_N8* satisfying_N9* satisfying_N10* satisfying_N11* satisfying_N12* satisfying_N13* satisfying_N14* satisfying_N15* satisfying_N16* satisfying_N17* satisfying_N18* satisfying_N19* Flow Petri Elements Pnet pre post Pre Post enter exit Prec Postc Entr Ext Input Output |^ 90 In_Power Newton_Coeff SetPrimes Prime SetPrimenumber primenumber is_Lipschitzian_on is_uniformly_continuous_on FinPairUnion 100 DISJOINT_PAIRS 100 Normal_forms_on 110 mi 110 NormForm 110 N-Str N-ZeroStr normF NORMSTR ||. .|| RealNormSpace-like RealNormSpace distance_by_norm_of MetricSpaceNorm TopSpaceNorm LinearTopSpaceNorm Norm_ NLin NVectQuot NKer InducedSur InducedBi NormCoset NormVSets ClNLin RAT_Sums ALGO_GCD ALGO_EXGCD ALGO_INVERSE ALGO_CRT NAT 255 REAL 255 COMPLEX 128 RAT 255 INT 255 ExtREAL value digits NPower ReciTriangRS SumsReciTriang geo-seq triangular mersenne Polygon -gonal IndexPoly polygonal CenterPolygon PolygonalNumbers TriangularNumbers SquareNumbers Topology_of Top_Union Top_Meet Open_setLatt F_primeSet StoneH 200 StoneS SF_have Set_Union Set_Meet StoneLatt HTopSpace dneg involutive TrivOrthoRelStr TrivPoset TrivAsymOrthoRelStr Dneg SubReFlexive SubIrreFlexive SubSymmetric SubAntisymmetric Asymmetric SubTransitive SubQuasiOrdered SubPreOrdered QuasiOrdered PreOrdered QuasiPure QuasiPureOrthoRelStr SubPartialOrdered PartialOrdered Pure PureOrthoRelStr SubStrictPartialOrdered StrictPartialOrdered StrictOrdered Orderinvolutive OrderInvolutive PreOrthoPoset QuasiOrthoComplement_on QuasiOrthocomplemented OrthoComplement_on Orthocomplemented QuasiOrthoPoset OrthoPoset Contravariant_Functor id* 128 *id 128 with_unique_fixpoint R_VectorSpace_of_ContinuousFunctions R_NormSpace_of_ContinuousFunctions Fredholm Choice_Function BOOL 122 Order being_quasi-order being_partial-order being_linear-order quasi_orders partially_orders linearly_orders has_upper_Zorn_property_wrt has_lower_Zorn_property_wrt is_maximal_in is_minimal_in is_superior_of is_inferior_of RelStr InternalRel Poset UpperCone 122 LowerCone 122 InitSegm 122 Initial_Segm Chains 122 disconnected POSet_set-like POSet_set MonFuncs Carr POSCat POSAltCat form_upper_lower_partition_of succ 128 epsilon-transitive epsilon-connected ordinal number Ordinal limit_ordinal Sequence-like Sequence c=-linear On 128 Lim 128 omega 128 natural limit Number last 128 inf 128 sup 200 Ordinal-yielding Ordinal-Sequence lim_sup 128 lim_inf 128 is_limes_of lim increasing continuous +^ 32 *^ exp is_cofinal_with -^ 32 div^ 32 mod^ 32 ^ 0-element_of 128 1-element_of 128 |^|^ epsilon first_epsilon_greater_than epsilon_ Sum^ Cantor-component -exponent Cantor-normal-form ord-type numbering criticals Ordinal-Sequence-valued lims OS@ OSV@ -Veblen ordinal-membered OrtSp-like OrtSp OSGeneratorSet osfree OSREL DTConOSA OSSym ParsedTerms PTDenOp PTOper ParsedTermsOSA LeastSort LeastSorts LCongruence FreeOSA PTClasses PTCongruence PTVars OSFreeGen NHReverse PTMin MinTerm MinTerms OverloadedMSSign Overloading RelSortedSign OverloadedRSSign order-sorted discernable op-discrete OSSign OrderSortedSign has_least_args_for has_least_sort_for has_least_rank_for ConstOSSet OrderSortedSet ConstOSA OSAlgebra OSAlg TrivialOSA OperNames OperName Name OrderSortedSubset OSSubset OSSubAlgebra OSConstants OSCl OSbool OSSubSort OSMSubSort GenOSAlg "\/"_os OSSub OSAlg_join OSAlg_meet OSSubAlLattice are_os_isomorphic os-compatible OrderSortedRelation OSCongruence Path_Rel locally_directed CompClass OSClass #_os OSQuotRes OSQuotArgs OSQuotCharact QuotOSAlg OSNat_Hom OSCng OSHomQuot being_a_square being_a_Sum_of_squares being_a_sum_of_squares being_a_Product_of_squares being_a_product_of_squares being_a_Sum_of_products_of_squares being_a_sum_of_products_of_squares being_an_Amalgam_of_squares being_an_amalgam_of_squares being_a_Sum_of_amalgams_of_squares being_a_sum_of_amalgams_of_squares being_a_generation_from_squares generated_from_squares c3add c3compl Relation4 ParStr 4_arg_relation '||' C_3 4C_3 PRs PR MPS ParSp-like ParSp FanodesSp-like FanodesSp is_collinear parallelogram congr PartFunc <: :> total PFuncs 128 tolerates TotFuncs 128 /. 100 positive-yielding negative-yielding nonpositive-yielding nonnegative-yielding '<' '>' is_a_dependent_set_of is_min_depend PARTITIONS '/\' '\/' ERl Rel %I %O satisfying_Int_Par_Pasch satisfying_Ext_Par_Pasch satisfying_Gen_Par_Pasch satisfying_Ext_Bet_Pasch satisfying_Int_Bet_Pasch ManySortedSet EmptyMS 250 overlaps overlap [= ManySortedFunction Component # *--> [| |] MSFuncs ManySortedSubset .:.: down ManySortedPartFunc total-yielding (Funcs) locally_finite clf paracompact Family_open_set TopSpaceMetr is_metric_of SpaceMetr metrizable PartUnion DisjointFam PartUnionNat [^ ^] transitive-yielding pcs-InternalRels TolStr ToleranceRel (--) pcs-tol-total pcs-tol-reflexive pcs-tol-irreflexive pcs-tol-symmetric emptyTolStr TolStr-yielding pcs-tol-reflexive-yielding pcs-tol-irreflexive-yielding pcs-tol-symmetric-yielding pcs-ToleranceRels ^`1 ^`2 pcs-Str pcs-compatible pcs-like anti-pcs-like pcs-total pcs anti-pcs pcs-empty pcs-singleton pcs-Str-yielding pcs-yielding pcs-chain-like pcs-Chain pcs-union MSSet pcs-sum pcs-extension pcs-reverse pcs-times pcs-self-coherent pcs-self-coherent-membered pcs-general-power-IR pcs-general-power-TR pcs-general-power pcs-coherent-power pcs-power <>* reproj is_partial_differentiable_in partdiff is_partial_differentiable_on `partial| SVF1 is_partial_differentiable`1_on is_partial_differentiable`2_on `partial1| `partial2| pdiff1 is_hpartial_differentiable`11_in is_hpartial_differentiable`12_in is_hpartial_differentiable`21_in is_hpartial_differentiable`22_in hpartdiff11 hpartdiff12 hpartdiff21 hpartdiff22 is_hpartial_differentiable`11_on is_hpartial_differentiable`12_on is_hpartial_differentiable`21_on is_hpartial_differentiable`22_on `hpartial11| `hpartial12| `hpartial21| `hpartial22| is_partial_differentiable`3_on `partial3| grad Directiondiff unitvector curl is_hpartial_differentiable`13_in is_hpartial_differentiable`23_in is_hpartial_differentiable`31_in is_hpartial_differentiable`32_in is_hpartial_differentiable`33_in hpartdiff13 hpartdiff23 hpartdiff31 hpartdiff32 hpartdiff33 is_hpartial_differentiable`13_on is_hpartial_differentiable`23_on is_hpartial_differentiable`31_on is_hpartial_differentiable`32_on is_hpartial_differentiable`33_on `hpartial13| `hpartial23| `hpartial31| `hpartial32| `hpartial33| PartDiffSeq is_partial_differentiable_up_to_order Block are_collinear closed_under_lines strong with_non_trivial_blocks identifying_close_blocks truly-partial without_isolated_points PLS non-void-yielding trivial-yielding non-Trivial-yielding PLS-yielding Segre-like Segre_Blocks Segre_Product Segre-Coset are_joinable Collineation permutation_of_indices 255 canonical_embedding segment pencil Pencils_of PencilSpace SubspaceSet GrassmannSpace PairSet PairSetFamily VeroneseSpace Crypto 128 order 128 Fermat 128 LinearPreorder Events_structure True False readE writeE procE traceE val_of events processes locations traces Process EventSet trace reads writesto val pr-complete pr-ordered rw-ordered rw-consistent rw-exclusive interval_in inter has_Peterson_mutex_in has_Peterson_mutex Values_with_TF Values_with_Bool DistributedSysWithSharedMem simultev PT_net_Str S-T_Arcs T-S_Arcs place places transition transitions S-T_arc T-S_arc Deadlock-like With_Deadlocks Trap-like With_Traps with_S-T_arc with_T-S_arc TrivialPetriNet cylinder0 thin_cylinder thin_cylinders Extcylinders Ristcylinders loc CylinderFunc Colored_PT_net_Str ColoredSet firing-rule outbound Outbds Colored-PT-net-like Colored-PT-net connecting-mapping connecting-firing-rule synthesis Colored_Petri_net TrivialColoredPetriNet Colored-PT-net-Family-like Colored-PT-net-Family color-threshold color-count colored-state Colored-states Cell-Petri-net Cell-Petri-nets is_Cell-Petri-nets XorDelta with-nontrivial-ColoredSet firable_set_on ptr_modetrans Ptr_Sub Ptr_Add firing_result decision_free_like Decision_free_PT places_and_trans_of With_directed_path directed_path_like With_directed_circuit places_of transitions_of is_firable_at is_not_firable_at num_marks nat_marks_of PetriNet Circuit_of_places_and_trans marking multitude_of {$} fire Petri_net firing-sequence process before concur NeutralProcess ElementaryProcess Polish-atoms Polish-expression-layer Polish-expression-hierarchy Polish-expression-set Polish-expression arity-from-list Polish-operations Polish-operation antichain-like antichain Polish-language Polish-arity-function Polish-arity-from-list exhaustive Polish-WFF-set Polish-WFF -headed -head -tail Polish-WFF-head Polish-arity Polish-WFF-args Polish-unOp Polish-binOp Polish-recursion-domain Polish-recursion-function -recursive mix-associative Formal-Series Subalgebra GenAlg Polynom-Algebra Polynom Quard Tri Four0 ^3 254 -real-root 1_root_of_cubic 2_root_of_cubic 3_root_of_cubic 1_root_of_quartic 2_root_of_quartic 3_root_of_quartic 4_root_of_quartic incidence-matrix PolyhedronStr PolytopsF IncidenceF polyhedron_1 polyhedron_2 polyhedron_3 polyhedron -polytopes eta -polytope-seq num-polytopes num-vertices num-edges num-faces -th-polytope incidence-value -chain-space -chains incidence-sequence Boundary -boundary -circuit-space -circuits -bounding-chain-space -bounding-chains -bounding-circuit-space -bounding-circuits simply-connected alternating-f-vector alternating-proper-f-vector alternating-semi-proper-f-vector eulerian Support Series 0_ Polynomial Polynom-Ring eval Polynom-Evaluation TuplesOrder Decomp prodTuples 0_. 1_. Leading-Monomial `^ is_a_root_of with_roots algebraic-closed Roots NormPolynomial FPower Polynomial-Function Compress univariate monomial-like Monomial Monom coefficient Constant ConstPoly emb pow mConv aConv is_primitive_root_of_degree DFT Vandermonde VM reduces_to is_reducible_wrt is_irreducible_wrt is_in_normalform_wrt top_reduces_to is_top_reducible_wrt PolyRedRel iterSet iter_min ConFuncs ConRelat ConPoset sup_func min_func least_fix_point fix_func chain-complete -image FlatPoset FlatConF FlatRelat FlatCarrier RecFunc01 BaseFunc01 RecFunc02 BaseFunc02 is_well_founded_with_minimal_set -root 200 to_power 120 log 200 number_e [[: :]] Inv 128 TrivialOp TrivialOps Trivial_Algebra Univ_Alg-yielding 1-sorted-yielding equal-signature ComSign ManySortedOperation equal-arity ComAr EmptySeq ProdOp ProdOpSeq ProdUnivAlg Commute MSAlgebra-Family SORTS OPER ?. OPS const MSAlgebra-Class are_mutually_disjoint PrefStr PIStr PreferenceStr PrefRel preference-like PreferenceSpace IdPrefSpace PrefSpace CharRel tournament-like flat IntPrefSpace PI-preference-like CharPrefSpace SymCl typealg left_quotient right_quotient inner_product type PreProof correct left right middle primitive represents does_not_represent free repr_of Proof cut-free size_w.r.t. cutdeg Model typestr derivability ==>. SynTypes_Calculus-like SynTypes_Calculus <==>. GeoSeq 120 -Root 120 #Z 120 #Q 120 Rational_Sequence #R 120 Fib Fusc FlattenSeq SgmX FinSequence-yielding ^^ support finite-support bag Bags EmptyBag BagOrder NatMinor divisors decomp TopStruct topology TopSpace-like TopSpace Point SubSpace Cl 128 T_0 T_1 T_2 normal T_3 T_4 idiv1_prg idiv_prg FS2XFS XFS2FS FS2XFS* XFS2FS* is_an_xrep_of IFLGT inner_prd_prg scalar_prd_prg vector_minus_prg vector_add_prg vector_sub_prg compl-closed Field_Subset SetSequence Complement non-ascending non-descending sigma-multiplicative SigmaField Probability sigma halfline Family_of_halflines Borel_Sets @Intersection @Complement disjoint_valued are_independent_respect_to .|. 110 Partial_Intersection Partial_Union Partial_Diff_Union @Partial_Intersection @Partial_Union @Partial_Diff_Union non-decreasing-closed non-increasing-closed MonotoneClass monotoneclass P2M M2P P_COM2M_COM ProbPart are_coplanar constitute_a_quadrangle |' configuration IncProjectivePlane is_a_triangle is_a_quadrangle Quadrangle IncProj are_concurrent CHAIN Projection -Group_over -Mult_over -VectSp_over Domain-Sequence BinOps UnOps AbGroup-yielding Group-Sequence addop complop zeros MultOps RealLinearSpace-yielding RealLinearSpace-Sequence multop RealNormSpace-yielding RealNormSpace-Sequence normsequence productnorm prod_ADD prod_MLT prod_ZERO prod_NORM with_max with_min RealMap pseudocompact W-bound N-bound E-bound S-bound SW-corner NW-corner NE-corner SE-corner W-most N-most E-most S-most W-min W-max N-min N-max E-max E-min S-max S-min IndexedPartition -index_of DomRel LimDomRel is_partitable_wrt is_exactly_partitable_wrt form_morphism_between is_rougher_than can_be_characterized_by square Pythagorean_triple degenerate simplified is_transformable_to QC-alphabet QC-symbols QC-symbol QC-variables 128 QC-variable bound_QC-variables 128 fixed_QC-variables 128 free_QC-variables 128 QC-pred_symbols 128 QC-pred_symbol -ary_QC-pred_symbols bound_QC-variable fixed_QC-variable free_QC-variable QC-variable_list -closed QC-WFF 128 QC-formula @ 128 VERUM 128 the_pred_symbol_of 20 the_arguments_of 20 still_not-bound_in 68 -one_in FALSUM 68 the_left_disjunct_of 66 the_right_disjunct_of 66 a. 68 Vars 68 Fixed 68 list_of_immediate_constituents tree_of_subformulae -entry_points_in_subformula_tree_of Subformula Entry_Point_in_Subformula_Tree entry_points_in_subformula_tree -expanding -Cast 129 -Consistent Probabilities QM_Str Observables FStates Quantum_Probability Obs Sts Meas Quantum_Mechanics-like Quantum_Mechanics OrthoRelStr is_an_involution is_a_Quantum_Logic Prop PropRel OrdRel InvRel QuantaleStr QuasiNetStr with_left-zero with_right-zero with_zero times-additive times-continuous Quantale QuasiNet BlikleNet inflationary deflationary times-monotone -r> -l> dualizing Girard-QuantaleStr absurd dualized Girard-Quantale Negation compquaternion addquaternion diffquaternion multquaternion divquaternion invquaternion G_Quaternion R_Quaternion QUATERNION quaternion Rea Im1 Im2 Im3 0q 1q Q. padd pmult QClass. Quot. qadd qmult q0. q1. qaddinv qmultinv quotadd quotmult quotaddinv quotmultinv the_Field_of_Quotients RingHomomorphism RingEpimorphism RingMonomorphism embedding RingIsomorphism is_embedded_in is_ringisomorph_to canHom has_Field_of_Quotients_Pair Radix 128 -SD 128 DigA 128 DigB 128 SubDigit 128 DigitSD 128 SDDec 128 DigitDC 128 DecSD 128 SD_Add_Carry 128 SD_Add_Data 128 is_represented_by Add 128 '+' 128 SubDigit2 128 DigitSD2 128 SDDec2 128 DigitDC2 128 DecSD2 128 Table1 128 Mul_mod 128 Table2 128 Pow_mod 128 -SD_Sub_S 128 -SD_Sub 128 SDSub_Add_Carry 128 SDSub_Add_Data 128 DigA_SDSub 128 SD2SDSubDigit 128 SD2SDSubDigitS 128 SD2SDSub 128 DigB_SDSub 128 SDSub2INTDigit 128 SDSub2INT 128 SDSub2IntOut 128 SDSubAddDigit 128 SDMinDigit 128 SDMin 128 SDMaxDigit 128 SDMax 128 FminDigit 128 Fmin 128 FmaxDigit 128 Fmax 128 M0Digit 128 M0 128 MmaxDigit 128 Mmax 128 MminDigit 128 Mmin 128 needs_digits_of MmaskDigit 128 Mmask 128 FSDMinDigit 128 FSDMin 128 is_Zero_over is_homogeneous_for ||^ Trivial-SigmaField Trivial-Probability Real-Valued-Random-Variable expect variance Real-Valued-Random-Variables-Set R_Algebra_of_Real-Valued-Random-Variables Product-Probability -Measure_valued -Probability_valued -Random-Variable-Family -random_variable-like random_variable random_variable_family-like random_variable_family image_measure probability -SigmaField_sequence-like SigmaField_sequence -Probability_sequence-like Probability_sequence Product_dom Trivial-SigmaField_sequence linear-transformation im rank nullity have_a_common_root have_no_common_roots have_common_roots is_a_common_root_of is_a_normalform_of reducible rational_function Leading-Coefficient LC NormRationalFunction NormRatF 0._ 1._ Common_Roots rational Rational compact closed open Neighbourhood IntervalCover IntervalCoverPts is_in Preserv || 100 is_Bin_Op_Preserv Presv ||| 100 DnT ! OnePoint add_2 mult_2 dL-Z_2 Field-like omf 188 revf 201 osf 199 ovf 188 Real integer-yielding Integer_Sequence modSeq 110 divSeq 110 remainders_for_scf 110 rfs 110 SimpleContinuedFraction 110 scf 110 convergent_numerators 110 convergent_denominators 110 c_n 110 c_d 110 convergents_of_continued_fractions 110 cocf 110 backContinued_fraction 110 bcf 110 minreal maxreal Real_Lattice maxfuncreal minfuncreal RealFunc_Lattice Euclid_add Euclid_mult Euclid_norm REAL-NS Euclid_scalar REAL-US terms've_same_card_as_number ascending lenght_equal_card_of_set RearrangmentGen Co_Gen Rland 200 Rlor 200 `1_3 `2_3 `3_3 `1_4 `2_4 `3_4 `4_4 `1_5 `2_5 `3_5 `4_5 `5_5 Relation-like Relation proj1 128 dom 128 proj2 128 rng 128 field 128 ~ 128 * non-empty id 128 | 100 |` 100 .: 100 " 128 empty-yielding Im 128 Coim -defined -valued is_reflexive_in is_irreflexive_in is_symmetric_in is_antisymmetric_in is_asymmetric_in is_connected_in is_strongly_connected_in is_transitive_in reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Reloc {_{ }_} .:^ $^ RedSequence reduces are_convertible_wrt is_a_normal_form_wrt is_a_normal_form_of are_convergent_wrt are_divergent_wrt are_convergent<=1_wrt are_divergent<=1_wrt has_a_normal_form_wrt nf co-well_founded weakly-normalizing strongly-normalizing commutes-weakly_with commutes_with with_UN_property with_NF_property subcommutative confluent with_Church-Rosser_property locally-confluent complete are_equivalent are_critical_wrt Completion XFinSequence-yielding ^+ semi-Thue-system Thue-system -->. ==>.-relation ==>* transition-system deterministic dim2 /^ MIM 128 max_p min_p sort_d sort_a max+ 200 max- 200 PartFunc-set PFUNC_DOMAIN addpfunc 200 CHI 128 is_common_for_dom is_convex_on FinS 200 is_strictly_convex_on is_quasiconvex_on is_strictly_quasiconvex_on is_strongly_quasiconvex_on is_upper_semicontinuous_in is_upper_semicontinuous_on is_lower_semicontinuous_in is_lower_semicontinuous_on inferior_realsequence superior_realsequence RingMorphismStr RingMorphism-like RingMorphism Ring_DOMAIN-like Ring_DOMAIN RingMorphism_DOMAIN-like RingMorphism_DOMAIN RingObjects RingCat quasi-prime quasi-maximal QuotientRing Unit NonUnit IntegralDomain PIDomain stagnating Ideals -homomorphic is_a_factorization_of factorizable uniquely_factorizable Factorization factorial FactorialRing deg* includes_an_isomorphic_copy_of includes '*' Z/ Char -characteristic CharSet carrier/\ PrimeField canHom_Int canHom_Rat canHom_Z/ -monomorphic Monomorphism -isomorphic Isomorphism -polynomial-membered -gcd a_gcd poly_mult_mod poly_mod Affin affinely-independent center_of_mass linearly-closed Subspace (0). 124 (Omega). 148 Coset Subspaces 154 is_the_direct_sum_of Linear_Compl SubJoin 124 SubMeet 124 LSeg convex-membered circled circled-membered RLTopStruct add-continuous Mult-continuous LinearTopSpace transl local_base locally-convex line RLSStruct Mult VECTOR Abelian add-associative right_zeroed RealLinearSpace-like Trivial-RLSStruct RealLinearSpace scalar-distributive vector-distributive scalar-associative scalar-unital vector 128 Linear_Combination Carrier 128 ZeroLC 128 LinComb 128 LCAdd 128 LCMult 128 LC_RLSpace 128 linearly-independent linearly-dependent Lin 128 Basis finite-dimensional dim Subspaces_of Z_Lin Submodule Submodules ComplStr Compl ComplLLattStr ComplULattStr OrthoLattStr TrivComplLat TrivOrtLat Robbins Huntington join-idempotent Bot 129 well-complemented preOrthoLattice CLatt with_idempotent_element \delta Expand _0 Double _1 _2 _3 _4 \beta de_Morgan satisfying_DN_1 satisfying_MD_1 satisfying_MD_2 join-Associative meet-Associative meet-Absorbing |_| |^| "|^|" "|_|" \/-SemiLattRelStr /\-SemiLattRelStr LattRelStr TrivLattRelStr OrthoLattRelStr TrivCLRelStr with_Top Ortholattice RelAugmentation LatAugmentation naturally_sup-generated naturally_inf-generated CLatAugmentation orthomodular Orthomodular_Lattice Orthomodular B_6 Benzene with_equivalence with_tolerance Approximation_Space Tolerance_Space LAp UAp BndAp rough exact RoughSet MemberFunc FinSeqM _c= c=^ _c=^ _= =^ _=^ Lap Uap is_serial_in is_mediate_in serial mediate empty-preserving universe-preserving Flip ClMap IntMap closed-valued open-valued is_positive_alliance_in is_negative_alliance_in is_alliance_in positive_alliance negative_alliance alliance GeneratedRelation GeneratedRelStr satisfying(7H') satisfying(7L') Meet 1stOpStr 2ndOpStr TwoOpStruct FirstOp SecondOp interior with_interior with_preinterior with_closure with_preclosure GenTopSpace extensive \/-preserving intensive /\-preserving preclosure preinterior op-closed op-open 1TopStruct 2TopStruct with_properly_defined_topology with_properly_defined_Topology with_op-closed_subsets with_op-open_subsets GenTop topology-like union-closed Natural naturally_generated map without_3rd_class_subsets El_ev Event prob are_independent the_set_of_RealSequences seq_id R_id l_add l_mult Zeroseq Linear_Space_of_RealSequences Add_ Mult_ Zero_ the_set_of_l2RealSequences l_scalar l2_Space RealHilbertSpace the_set_of_l1RealSequences l_norm l1_Space CCauchy Cauchy_sequence_by_Norm the_set_of_BoundedRealSequences linfty_norm linfty_Space BoundedFunctions R_VectorSpace_of_BoundedFunctions BoundedFunctionsNorm R_NormSpace_of_BoundedFunctions Affine Up Subspace-like is_parallel_to Ort_Comp TopUnitSpace sqrreal 128 sqr 128 mlt 128 complex-yielding |( )| are_orthogonal sqrcomplex are_gamma-equivalent Mean GMean HetSet Het heterogeneous Homogen MeanLess MeanMore bubble-sort Bubble-Sort-Algorithm Sorting-Function Directed Macro Initialized ";" 32 IExec paraclosed parahalting keeping_0 Initialize refers refer destroys destroy good is_halting_on Goto is_pseudo-closed_on pseudo-paraclosed pseudo-LifeSpan if=0 if>0 if<0 loop Times ProperBodyWhile=0 WithVariantWhile=0 ExitsAtWhile=0 ProperBodyWhile>0 WithVariantWhile>0 ExitsAtWhile>0 on_data_only Fusc_macro SCM+FSA-Data-Loc SCM+FSA-Data*-Loc SCM+FSA-Memory SCM+FSA-Instr SCM+FSA-OK SCM+FSA-State SCM+FSA-Chg int_addr1 int_addr2 coll_addr1 int_addr3 coll_addr2 SCM+FSA-Exec-Res SCM+FSA-Exec int_addr SCM+FSA Int-Locations FinSeq-Locations Int-Location FinSeq-Location intloc insloc fsloc :=len :=<0,...,0> :==1 Load aSeq while=0 while>0 while<0 StepWhile=0 StepWhile>0 insert-sort Insert-Sort-Algorithm SCMPDS-Instr SCMPDS-OK SCMPDS-State Address_Add const_INT P21address P22const P31address P32const P33const P41address P42address P43const P44const PopInstrLoc RetSP RetIC SCMPDS-Exec SCMPDS Int_position DataLoc return saveIC <>0_goto <=0_goto >=0_goto ICplusConst stop valid_at shiftable No-StopCode if<>0 if<=0 if>=0 for-down Dstate intpos GBP SBP GCD-Algorithm const_address const_value -at_most_dimensional finitely_colorable SimpleGraph-like PairsOf Edges SubgraphInducedBy MycielskianSeq Mycielski'sSeq CompleteSGraph edgeless pairfree State-consisting SCM-AE bin-term -Meaning_on Selfwork SCM-Compile d". max_Data-Loc_in InitClosed InitHalting keepInt0_1 is_closed_onInit is_halting_onInit while<>0 is_FinSequence_on Partition QuickSort Semi_Affine_Space-like Semi_Affine_Space sum opposite trap qtrap Functional_Sequence common_on_dom is_point_conv_on is_unif_conv_on monotone Real_Sequence convergent upper_bound 128 lower_bound 128 Partial_Sums 250 summable absolutely_summable Partial_Product 250 meet 128 is_finer_than is_coarser_than UNION INTERSECTION DIFFERENCE Subset-Family COMPLEMENT with_non-empty_elements Intersect empty-membered with_non-empty_element Cover with_proper_subsets inferior_setsequence superior_setsequence (/\) (\/) 32 (\) 32 (\+\) 30 {}. 150 having_a_unity {. .} $$ 80 FinUnion 150 singleton 150 finSeg RWNotIn-seq -thRWNotIn -stRWNotIn -ndRWNotIn -rdRWNotIn -thNotUsed -stNotUsed -ndNotUsed -rdNotUsed Fib_macro times StepTimes ProperTimesBody triv-times Fib-macro times* StepForUp ProperForUpBody for-up FinSeqMin Selection-sort UsedILoc UsedI*Loc UsedIntLoc UsedInt*Loc read-only read-write FirstNotIn FirstNotUsed First*NotIn First*NotUsed nat_interval TWOELEMENTSETS SimpleGraphStruct SEdges SIMPLEGRAPHS SimpleGraph is_isomorphic_to is_SetOfSimpleGraphs_of SubGraph degree is_path_of PATHS is_cycle_of K_ TriangleGraph upper-bounded' Top' lower-bounded' Bot' distributive' is_a_complement'_of complemented' `# 100 meet-idempotent ShefferStr stroke ShefferLattStr ShefferOrthoLattStr TrivShefferOrthoLattStr properly_defined satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 satisfying_Sh_1 SimplicialComplexStr 2SF_of subset-closed_closure_of SimplicialComplex Complex_of SubSimplicialComplex simplex-like -Simplex Simplex -standardComplex with_empty_element Skeleton_of the_subsets_with_limited_card c=-linearSeq_of subdivision vertex-like Vertices finite-vertices locally-finite BCS simplex-join-closed SubdivisionStr Subdivision Lebesgue_number -bounded arcsec1 arcsec2 arccosec1 arccosec2 CHK Prod_complex_n Prod_real_n !c ExpSeq rExpSeq Coef Coef_e Expan Expan_e Alfa Conj sin cos P_sin P_cos exp_R P_dt P_t tan cot PI sinh cosh tanh sin_C cos_C sinh_C cosh_C cosec sec coth sech cosech arcsin arccos sinh" cosh1" cosh2" tanh" coth" sech1" sech2" csch" arctan arccot is_extremal_in horizontal vertical alternating are_generators_of S-Sequence_in_R2 split special_polygonal Special_polygon_in_R2 SpStSeq rectangular is_in_the_area_of is_a_h.c._for is_a_v.c._for clockwise_oriented ^2 254 sqrt 200 cap-finite-partition-closed diff-finite-partition-closed diff-c=-finite-partition-closed with_countable_Cover semiring_of_sets sring4_8 semi-diff-closed semialgebra_of_sets Ring_generated_by Field_generated_by SigmaRing sigmaring Semiring DisUnion semidiff capOpCl SemiringFamily SemiringProduct cap-closed-yielding ClassicalSemiringFamily MeasurableRectangle OpenHypercubesRAT object2RAT the_set_of_all_left_open_real_bounded_intervals the_set_of_all_right_open_real_bounded_intervals the_set_of_all_closed_real_bounded_intervals the_set_of_all_open_real_bounded_intervals dense_countable_OpenHypercubes ProductREAL ProductLeftOpenIntervals ProductRightOpenIntervals ClosedHyperInterval OpenHyperInterval LeftOpenHyperInterval RightOpenHyperInterval Infty_dist EMINFTY TOP-REAL-INFTY StackSystem s_empty s_push s_pop s_top stack emp pop push top StandardStackSystem pop-finite push-pop top-push pop-push push-non-empty proper-for-identity StackAlgebra ==_ /== form_isomorphism_between coset core ConstructionRed "increasing block 'increasing 1-sorted carrier ZeroStr ZeroF OneStr OneF ZeroOneStr degenerated 2-sorted carrier' void trivial' NonZero Val_Sub Val_S CQCSub_& CQC-WFF-like CQCSub_All CQCSub_the_scope_of CQCQuant NEx_Val RSub1 RSub2 Element Subset [#] 128 ` 150 choose proper SubstitutionSet SubstLatt vSUB CQC_Substitution CQC_Subst RestrictSub Bound_Vars Dom_Bound_Vars Sub_Var NSub upVar ExpandSub PQSub QSub QC-Sub-closed QC-Sub-WFF Sub_P Sub_VERUM Sub_not Sub_& quantifiable second_Q_comp Sub_All Sub_atomic Sub_negative Sub_conjunctive Sub_universal Sub_the_arguments_of Sub_the_argument_of Sub_the_left_argument_of Sub_the_right_argument_of Sub_the_bound_of Sub_the_scope_of S_Bound Quant CQC_Sub CQC-Sub-WFF -Sub-closed -Sub_VERUM Sbst CFQ QScope Qsc PATH R_eal SetMajorant SetMinorant bool_DOMAIN SUP INF 0. 128 Denum_Set_of_R_EAL nonnegative Ser 200 SUM SymStr _|_ SymSp-like SymSp ProJ PProJ CL c= union 128 are_equipotent Classification Strong_Classification low_toler fam_class are_in_tolerance_wrt dist_toler fam_class_metr with_superior with_comparable_down hierarchic Hierarchy mutually-disjoint with_max's log_ ln Taylor Maclaurin totally_bounded Two_Divisible Two_Divisible_Group Uniquely_Two_Divisible_Group CONGRD AV ==> AffVect-like AffVect Domains_of Domains_Union D-Union Domains_Meet D-Meet Domains_Lattice Closed_Domains_of Closed_Domains_Union CLD-Union Closed_Domains_Meet CLD-Meet Closed_Domains_Lattice Open_Domains_of Open_Domains_Union OPD-Union Open_Domains_Meet OPD-Meet Open_Domains_Lattice domains-family closed-domains-family open-domains-family anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected HT HM Red cobool ADTS STS Sspace maximal_discrete anti-discrete-set-family MaxADSF maximal_anti-discrete MaxADSet MaxADSspace is_absolutely_bounded_by ClosedHypercube is_continuous_at is_not_continuous_at -extension_of_the_topology_of modified_with_respect_to modid Total TolSet TolClass-like TolClass neighbourhood TolSets TolClasses Paths Loops FundamentalGroup pi_1 pi_1-iso RealHomotopy ConvexHomotopy R1Homotopy FundGrIso Gr2Iso FGPrIso ExtendInt Prj1 Prj2 cLoop Ciso simply_connected having_trivial_Fundamental_Group nullhomotopic parametrized-curve with_first_point with_last_point with_endpoints Curve Curves the_first_point_of the_last_point_of LoopMlt 110 inverse_loop 110 HomotopyMlt 110 HopfHomotopy 110 R^1-TIMES 110 I[01]-TIMES 110 Seq_of_ind with_finite_small_inductive_dimension finite-ind ind is_an_accumulation_point_of Der is_isolated_in dense-in-itself perfect scattered density separable Chi Neighborhood_System finite-weight infinite-weight DiscrWithInfin point-filtered Sorgenfrey-line is_local_minimum_of continuum -powers ClFinTop -PointClTop -DiscreteTop TotFam all-open-containing all-closed-containing closed_for_countable_unions closed_for_countable_meets F_sigma G_delta T_1/2 is_a_condensation_point_of BorelSets Borel y=0-line y>=0-plane Niemytzki-plane Tychonoff Sorgenfrey-plane real-anti-diagonal Homeomorphism HomeoGroup TopGrStr UnContinuous BinContinuous TopGroup TopologicalGroup Closed-Interval-MSpace being_ball-family R^1 Closed-Interval-TSpace sequentially_compact is_an_arc_of R^2-unit_square L~ special unfolded s.n.c. being_S-Seq being_S-P_arc north_halfline east_halfline south_halfline west_halfline being_simple_closed_curve Simple_closed_curve is_S-P_arc_joining being_special_polygon being_Region max-Prod2 Trectangle R2Homeomorphism IntIntervals Tcircle Tunit_circle c[10] c[-10] Topen_unit_circle CircleMap Circle2IntervalR Circle2IntervalL TIMES 100 PROJ 100 Int 128 Fr 128 dense boundary nowhere_dense condensed closed_condensed open_condensed being_homeomorphism everywhere_dense is_FormalIz_of is_automorphism_of is_DIL_of CongrSpace-like CongrSpace positive_dilatation negative_dilatation dilatation translation collineation L[01] 180 P[01] 180 is_a_prefix_of is_a_proper_prefix_of ProperPrefixes 128 Tree-like Tree elementary_tree 128 Leaves Leaf Subtree with-replacement AntiChain_of_Prefixes-like AntiChain_of_Prefixes height 128 width 128 finite-order Chain Level -level Branch-like Branch DecoratedTree-like DecoratedTree branchdeg Trees FinTrees constituted-Trees constituted-FinTrees constituted-DTrees DTree-set Tree-yielding FinTree-yielding DTree-yielding T-Substitution roots Node root-tree -flat_tree -tree root finite-branching Subtrees FixedSubtrees -Subtrees -ImmediateSubtrees tree symplexes lower_non-empty FuncsSeq NatEmbSeq triangulation TriangStr SkeletonSeq FacesAssign Symplex Face face Triang are_not_separated are_weakly_separated are_not_weakly_separated constitute_a_decomposition do_not_constitute_a_decomposition Kolmogorov_space non-Kolmogorov_space Kolmogorov_subspace non-Kolmogorov_subspace maximal_T_0 maximal_Kolmogorov_subspace Stone-retraction SegM Prefix TuringStr Symbols AcceptS Tape Tape-Chg All-State Tran-Source Tran-Goal offset Head TRAN Accept-Halt Sum_Tran is_1_between storeData SumTuring computes Succ_Tran SuccTuring Zero_Tran ZeroTuring U3(n)Tran U3(n)Turing UnionSt FirstTuringTran SecondTuringTran FirstTuringState SecondTuringState FirstTuringSymbol SecondTuringSymbol Uniontran UnionTran ';' 32 and2 and2a and2b nand2 nand2a nand2b or2 or2a or2b nor2 nor2a nor2b xor2 xor2a xor2b and3 and3a and3b and3c nand3 nand3a nand3b nand3c or3a or3b or3c nor3 nor3a nor3b nor3c xor3 CompStr CompCirc CompOutput IncrementStr IncrementCirc IncrementOutput BitCompStr BitCompCirc are_homeomorphic Indiscernibility Indiscernible T_0-reflex T_0-canonical_map T_0-TopSpace Closed_Partitions T_1-reflex T_1-reflect homogeneous PFuncFinSequence UAStr charact Universal_Algebra arity 128 signature PFuncsDomHQN Operations operation is_closed_on opers_closed Opers 128 SubAlgebra UniAlgSetClosed Constants with_const_op GenUnivAlg Sub UniAlg_join UniAlg_meet UnSubAlLattice SubAlgebra-Family [~] entourages UniformSpaceStr Uniform_Space TrivialUniformSpace NonEmptyTrivialUniformSpace axiom_U1 axiom_U2 axiom_U3 Quasi-UniformSpace Semi-UniformSpace axiom_UL Locally-UniformSpace UniformSpace axiom_UP1 axiom_UP3 FMT_induced_by TopSpace_induced_by block_Pervin_quasi_uniformity subbasis_Pervin_quasi_uniformity basis_Pervin_quasi_uniformity Pervin_quasi_uniformity uniformity_induced_by axiom_UP2 element_left_uniformity system_left_uniformity element_right_uniformity system_right_uniformity left_uniformity right_uniformity UniformSpaceStr2RelStr RelStr2UniformSpaceStr partition_topology InternalRel2Uniformity Uniformity2InternalRel InternalRel2Element fundamental_element_of_entourages fundamental_system_of_entourages block_Pervin_uniformity subbasis_Pervin_uniformity basis_Pervin_uniformity Pervin_uniform_space MultGroup -roots_of_1 -th_roots_of_1 unital_poly cyclotomic_poly canFS -bag Rbag poly_shift poly_quotient multiplicity BRoots fpoly_mult_root poly_with_roots dyadic DYADIC dyad axis Nbhd Between Drizzle Rain inf_number_dyadic Tempest Rainbow Thunder Valuations_in FOR_ALL interpretation Valid complex-valued ext-real-valued real-valued rational-valued integer-valued natural-valued non-zero decreasing non-decreasing non-increasing subsequence zeroed (#) /" Shift DOMS complex-functions-membered ext-real-functions-membered real-functions-membered rational-functions-membered integer-functions-membered natural-functions-membered C_PFuncs C_Funcs E_PFuncs E_Funcs R_PFuncs R_Funcs Q_PFuncs Q_Funcs I_PFuncs I_Funcs N_PFuncs N_Funcs complex-functions-valued ext-real-functions-valued real-functions-valued rational-functions-valued integer-functions-valued natural-functions-valued (/) <-> (-) 32 128 [+] [-] [/] 128 <+> <#> 128 <++> <--> <##> 128 128 internal Geometry isometric ISOM RLSMetrStruct translatible Norm RealLinearMetrSpace RLMSpace IsomGroup SubIsomGroupRel StructVectSp CosetSet addCoset zeroCoset lmultCoset VectQuot coeffFunctional ker QFunctional CQFunctional with_eigenvalues eigenvalue eigenvector UnionKers G_Real AddGroup AbGroup right-distributive left-distributive right_unital F_Real well-unital left_unital Field ModuleStr lmult Scalar Vector comp VectSp-like VectSp Fanoian comRing domRing-like domRing Skew-Field RightModStr rmult BiModStr AbGr LeftModule RightModule BiModule LeftMod RightMod-like RightMod BiMod-like BiMod SubVS-Family FuncLatt Semilattice-Homomorphism sup-Semilattice-Homomorphism is_bounded_on ClOpers System ClosureSystems ClImageMap closure_op DsupClOpers Subalgebras inaccessible_by_directed_joins closed_under_directed_sups property(S) directly_closed Scott is_S-limit_of Scott-Convergence Net-Str jointly_Scott-continuous atom ATOM CLHomomorphism is_FG_set completely-irreducible Irr ,... SCMaps TopStruct-yielding product_prebasis is_Retract_of Sierpinski_Space TopPoset Lawson EqRel CLCongruence kernel_op kernel_congruence SemilatticeHomomorphism Embedding lim_infs-preserving is_FreeGen_set_of FixedUltraFilters -extension_to_hom infs-closed sups-closed weight second-countable CLbasis with_bottom with_top supMap idsMap baseMap ContMaps Omega monotone-convergence -POS_prod -TOP_prod oContMaps *graph uncurrying currying commuting UPS greater_or_equal_to_id lim_inf-Convergence xi Sigma Theta ^0 with_small_semilattices with_compact_semilattices with_open_semilattices CLweight Way_Up order_consistent inf_net lim-inf Xi LowerAdj UpperAdj -INF_category -SUP_category waybelow-preserving relatively_open -INF(SC)_category -SUP(SO)_category -CL_category -CL-opp_category compact-preserving finite-sups-preserving bottom-preserving finite-sups-inheriting bottom-inheriting extra-order -LowerMap strict_chain Strict_Chains is_inductive_wrt satisfies_SIC_on satisfying_SIC SetBelow sup-closed SupBelow directed filtered filtered-infs-inheriting directed-sups-inheriting antitone NetStr mapping prenet net netmap is_eventually_in is_often_in eventually-directed eventually-filtered downarrow uparrow lower upper Ids Filt Ids_0 Filt_0 finsups fininfs Semilattice sup-Semilattice LATTICE preserves_inf_of preserves_sup_of infs-preserving sups-preserving meet-preserving join-preserving filtered-infs-preserving directed-sups-preserving up-complete /\-complete ex_min_of ex_max_of has_the_min_in has_the_max_in is_minimum_of is_maximum_of Connection Galois upper_adjoint lower_adjoint projection closure kernel corestr inclusion FinSups inf_op sup_op satisfying_MC meet-continuous is_way_below << >> isolated_from_below waybelow wayabove satisfying_axiom_of_approximation non-Empty reflexive-yielding locally-compact -waybelow IntRel auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary Aux AuxBottom -below -above MonSet Rel2Map Map2Rel DownMap approximating App satisfying_SI satisfying_INT is_directed_wrt is_maximal_wrt is_minimal_wrt DoubleIndexedSet \// /\\ Sups Infs completely-distributive CLSubFrame Open meet-irreducible join-irreducible IRR order-generating PRIME co-prime is_a_cluster_point_of is_a_convergence_point_of pseudoprime CompactSublatt compactbelow satisfying_axiom_K algebraic arithmetic +id opp+id TopRelStr TopLattice Centralizer -con_map conjugate_Classes centralizer VectSp_over_center dist_max dist_min min_dist_min max_dist_min min_dist_max max_dist_max well_founded-Part is_recursively_expressed_by descending -Seg 128 well_founded is_well_founded_in well-ordering well_orders |_2 100 is_isomorphism_of are_isomorphic canonical_isomorphism_of 100 RelIncl 128 order_type_of 32 is_order_type_of FALSE TRUE boolean 'not' 82 '&' 80 'or' 70 => 69 <=> 69 'nand' 'nor' 'xor' '\' empty {} 128 \/ 32 /\ \ 32 \+\ 30 misses c< are_c=-comparable meets complex zero Complex real triple quadruple proj1_3 proj2_3 proj3_3 proj1_4 proj2_4 proj3_4 proj4_4 ext-real +infty 200 -infty 200 <= >= > positive negative min 128 max 128 IFGT ExtReal [. .] .[ ]. UpperBound LowerBound left_end right_end bounded_below bounded_above bounded real-bounded N_5 M_3 [# #] basis topological_semilattice MergeSequence Components in_general_position is_a_retraction_of is_an_UPS_retraction_of is_an_UPS_retract_of Poset-yielding inherits_sup_of inherits_inf_of are_opposite dualizing-func are_dual para-functional -carrier_of the_carrier_of set-id-inheriting concrete Concretized Concretization NeighborhoodSystem a_filter a_net have_the_same_composition are_isomorphic_under are_anti-isomorphic_under as_1-sorted 255 POSETS carrier-underlaid lattice-wise with_complete_lattices with_all_isomorphisms -UPS_category -CONT_category -ALG_category ex_sup_of ex_inf_of SubRelStr subrelstr meet-inheriting join-inheriting infs-inheriting sups-inheriting InclPoset BoolePoset RelStr-yielding MonMaps SupMap IdsMap \\/ //\ Sup Inf [" "] the_universe_of yielding_non-empty_carriers ConstantNet SubNetStr subnet NetUniv net_set Iterated OpenNeighborhoods Convergence-Class Convergence (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) ConvergenceSpace topological ComplMap -quasi_basis Baire irreducible is_dense_point_of sober CofinTop TopAugmentation TopExtension Refinement EnsHom <| ,?> Yoneda bool 128 [: :] are_mutually_distinct trivial def_func' def_func is_definable_in is_parametrically_definable_in <==> is_elementary_subsystem_of ZF-axioms 200 Collapse 128 is_epsilon-isomorphism_of are_epsilon-isomorphic decode 128 x". 200 code 128 Diagram 128 closed_wrt_A1 closed_wrt_A2 closed_wrt_A3 closed_wrt_A4 closed_wrt_A5 closed_wrt_A6 closed_wrt_A7 closed_wrt_A1-A7 Section predicatively_closed VAR 128 Variable x. 200 '=' 90 'in' 90 WFF 68 ZF-formula-like ZF-formula being_equality being_membership conjunctive atomic disjunctive conditional biconditional existential Var1 66 Var2 66 the_argument_of 66 the_left_argument_of 66 the_right_argument_of 66 bound_in 66 the_scope_of 66 the_antecedent_of 66 the_consequent_of 66 the_left_side_of 66 the_right_side_of 66 is_immediate_constituent_of is_subformula_of is_proper_subformula_of Subformulae 66 variables_in 68 Free 72 VAL 72 St 72 |= the_axiom_of_extensionality 128 the_axiom_of_pairs 128 the_axiom_of_unions 128 the_axiom_of_infinity 128 the_axiom_of_power_sets 128 the_axiom_of_substitution_for 128 being_a_model_of_ZF Subclass DOMAIN-yielding DOMAIN-Sequence inttorealM realtointM mltI Coordinate BilinearM GramMatrix GramDet LatticeStr Z_Lattice-like Z_Lattice Z_Sublattice INTegral positive-definite FrForm NulFrForm 0FrFunctional FrFunctionalFAF FrFunctionalSAF FrFunctional FrFormFunctional bilinear-FrForm linear-FrFunctional GenLat <; ;> Z_ModuleStruct Trivial-Z_ModuleStruct Z_Module Mult-cancelable with_Linear_Compl Int-mult-left Z_Linear_Combination Z_ZeroLC LC_Z_Module Mult_INT* Z_ModuleQuot Mult_Mod_pV Z_MQ_VectSp ZMtoMQV finite-rank EQRZM MorphsZQ Submodules_of @* lCFST torsion torsion-free torsion_part ZQMorph Zdecom Rat-Module divisible EMbedding DivisibleMod