summaryrefslogtreecommitdiff
path: root/library/topology
AgeCommit message (Collapse)Author
2024-09-23AbgabeSimon-Kor
2024-09-23working commitSimon-Kor
2024-09-18Ambiguous parseSimon-Kor
in urysohn2.tex line 674 the secound 2 throws an ambiguous parse. the same definition in line 678 commented without this a does not throe this error. ambiguous parse: [BlockLemma (SourcePos {sourceName = "set.tex", sourceLine = Pos 129, sourceColumn = Pos 1}) (Marker "empty_eq") (Lemma [] (StmtConnected Implication (StmtVerbPhrase (TermExpr (ExprVar (NamedVar "x")) :| [TermExpr (ExprVar (NamedVar "y"))]) (VPAdj (Adj [Just (Word "empty")] [] :| []))) (StmtFormula (FormulaChain (ChainBase (ExprVar (NamedVar "x") :| []) Positive (RelationSymbol (Symbol "=")) (ExprVar (NamedVar "y") :| [])))))),BlockLemma (SourcePos {sourceName = "set.tex", sourceLine = Pos 129, sourceColumn = Pos 1}) (Marker "empty_eq") (Lemma [] (StmtConnected Implication (StmtConnected Conjunction (StmtVerbPhrase (TermExpr (ExprVar (NamedVar "x")) :| []) (VPVerb (Verb (SgPl {sg = [], pl = []}) []))) (StmtVerbPhrase (TermExpr (ExprVar (NamedVar "y")) :| []) (VPAdj (Adj [Just (Word "empty")] [] :| [])))) (StmtFormula (FormulaChain (ChainBase (ExprVar (NamedVar "x") :| []) Positive (RelationSymbol (Symbol "=")) (ExprVar (NamedVar "y") :| []))))))]
2024-09-18working commitSimon-Kor
2024-09-17working commitSimon-Kor
2024-09-17Corrected Math Env ParsingSimon-Kor
Since Latex has a really specify syntax for \begin{cases} ... \end{cases} The math mode in tokenizing had to be setup correctly.
2024-09-16Topo Space Real VerficationSimon-Kor
2024-09-16working commitSimon-Kor
2024-09-16Finished proof of topological basisSimon-Kor
2024-09-16working commitSimon-Kor
2024-09-16Missmatched Assume Error found. not fixedSimon-Kor
In line 137 and 140 of real-topological-space.tex Line 140 wont get parsed and line 140 will get parsed. Case matching in Checking.hs is not working as intended. Case phi@(Atomic p args) -> in line 960 in checking.hs is not reached in checking of the Fixing with a symbol Error Massage shows that < will be interpreted as a Term symbol there not as a predicate. Error Massage: zf: MismatchedAssume (TermSymbol (SymbolPredicate (PredicateRelation (Symbol "<"))) [TermVar (NamedVar "c"),TermVar (NamedVar "x")]) (Connected Implication (TermSymbol (SymbolPredicate (PredicateRelation (Command "rless"))) [TermVar (NamedVar "c"),TermVar (NamedVar "x")]) (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (NamedVar "c"),TermSymbol (SymbolMixfix [Just (Command "epsBall"),Just InvisibleBraceL,Nothing,Just InvisibleBraceR,Just InvisibleBraceL,Nothing,Just InvisibleBraceR]) [TermVar (NamedVar "x"),TermVar (NamedVar "epsilon")]]))
2024-09-15Fix Assume IssueSimon-Kor
At line 137 in real-topological-space.tex Can't use Fix at this point.
2024-09-15Issue at Fixing.Simon-Kor
In Line 49 in real-topological-space.tex the Fix can't be processed.
2024-09-05Precondtion failed in line 161 urysohn2.texSimon-Kor
Error: zf: Precondition failed in encodeTerm, cannot encode terms with comprehensions directly: TermSep (NamedVar "n") (TermSymbol (SymbolMixfix [Just (Command "naturals")]) []) (Scope (TermSymbol (SymbolPredicate (PredicateRelation (Command "rless"))) [TermSymbol (SymbolInteger 1) [],TermVar (B ())])) CallStack (from HasCallStack): error, called at source/Encoding.hs:89:13 in zf-0.3.0.0-3mIpbM9y9fK3yXjxxoLDb2:Encoding
2024-09-05working commitSimon-Kor
2024-09-04working commitSimon-Kor
2024-09-04Mismatched Assume in InductionSimon-Kor
Unexpeced Mismatch in line 99 and 109 or the pair 100 and 108. Parsing works with line 99 and 108 or with the lines 100 and 109. zf: MismatchedAssume (TermSymbol (SymbolPredicate (PredicateNoun (SgPl {sg = [Just (Word "natural"),Just (Word "number")], pl = [Just (Word "natural"),Just (Word "numbers")]}))) [TermVar (NamedVar "n")]) (Connected Implication (TermSymbol (SymbolPredicate (PredicateRelation (Command "in"))) [TermVar (NamedVar "n"),TermSymbol (SymbolMixfix [Just (Command "naturals")]) []]) (TermSymbol (SymbolPredicate (PredicateVerb (SgPl {sg = [Just (Word "has"),Just (Word "cardinality"),Nothing], pl = [Just (Word "ha"),Just (Word "cardinality"),Nothing]}))) [TermSymbol (SymbolMixfix [Just (Command "seq"),Just InvisibleBraceL,Nothing,Just InvisibleBraceR,Just InvisibleBraceL,Nothing,Just InvisibleBraceR]) [TermSymbol (SymbolMixfix [Just (Command "emptyset")]) [],TermVar (NamedVar "n")],TermSymbol (SymbolMixfix [Just (Command "suc"),Just InvisibleBraceL,Nothing,Just InvisibleBraceR]) [TermVar (NamedVar "n")]]))
2024-09-03working commitSimon-Kor
2024-09-03Finished induction beginSimon-Kor
2024-09-02working commitSimon-Kor
2024-09-02working commitSimon-Kor
2024-09-02Corrected Contradiction.Simon-Kor
Contradiction was due to a misstake in the definition in sequence.
2024-08-31Contradiction in sequenceSimon-Kor
False can be proven with iff_sequence, codom_of_emptyset_can_be_anything,sequence, emptyset_is_function_on_emptyset,id_dom,in_irrefl, suc_subseteq_implies_in,emptyset_subseteq
2024-08-31working commitSimon-Kor
2024-08-30working commitSimon-Kor
2024-08-29working commitSimon-Kor
2024-08-28working commitSimon-Kor
2024-08-27working commitSimon-Kor
2024-08-27Feature CompleteSimon-Kor
Finalised the proof output and goals. The Local Function definition now producces a Function f with the right domain and range, together with the rules presented in cases. Then proof goal of this local definition is set to for all x we have x is element of dom(f) if and only if x is in exactly one of the subdomains. This suffices as welldefindness check on f, besides the right range. Further checks that should be implemented are the correct range of the function. And optional subproof such that the presented goal can be check easily.
2024-08-27ambigus parse fix. The proof goal must be changed,Simon-Kor
since now some could define a function with overlapping and worng subdomains
2024-08-27Experimental working commit, programm will compileSimon-Kor
But the Proof that the domain of the local function is not right. Also if in the definition of our local function we just use f(x) = x then we get a technical ambigus parse
2024-08-24naproch sty extensionSimon-Kor
2024-08-14The added proposition and definition should haveSimon-Kor
resloved some proofing complications, but they can prove flase together with lemmas about ordinal, the exat lemma are in urysohn.tex at line 522.
2024-08-13less urysohnSimon-Kor
2024-08-12way way way way more urysohnSimon-Kor
2024-08-12way way way more urysohnSimon-Kor
2024-08-12way way more urysohnSimon-Kor
2024-08-12way more urysohnSimon-Kor
2024-08-12Completed the structure of the proof of Urysohn.Simon-Kor
Now every single step has to be proven.
2024-08-12more more way more urysohnSimon-Kor
2024-08-11more more more urysohnSimon-Kor
2024-08-10more more urysohnSimon-Kor
2024-08-10more urysohnSimon-Kor
2024-08-10more ur<sohnSimon-Kor
2024-08-09put cardinalit to the right placeSimon-Kor
2024-08-07Created first urysohn formalizationSimon-Kor
2024-06-25[Stable] Implented continuous.tex and omitted some provesSimon-Kor
All changes till here are done such that the check of everything.tex will be a success. There are no logic flaws and false can't be proven with everything out of everthing.tex
2024-06-25Improvement for the ATP proof timeSimon-Kor
2024-06-20[Stable] Topologgical-space.texSimon-Kor
2024-06-20[Report] Task failed and was proven in the same time.Simon-Kor
The Line 182 has the goal to apply regular in a topological space. But if i try to prove it with Naproche ZF, then the task will be proven and the task fails in the same time. Console Output is the following: time stack exec zf -- --log library/topology/separation.tex -t 30 --dump ./dump [Info] 00:00.11 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,elem(fx,fB)&subseteq(fB,setminus(s__carrier(fX),fA))&subseteq(setminus(s__carrier(fX),fA),fU)). [Info] 00:00.11 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,setminus(s__carrier(fX),setminus(s__carrier(fX),fU))=fU). [Info] 00:00.11 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,?[XN]:(elem(XN,neighbourhoods(fx,fX))&subseteq(XN,fU)&is_closed_in(XN,fX))). [Info] 00:00.21 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,(is_regular(fX)&is_kolmogorov(fX))<=>![XU]:(elem(XU,s__opens(fX))=>![Xx]:(elem(Xx,XU)=>?[XN]:(elem(XN,neighbourhoods(Xx,fX))&subseteq(XN,XU)&is_closed_in(XN,fX))))). [Info] 00:02.34 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,?[XB,XA]:(elem(fx,XB)&subseteq(fC,XA)&inter(XA,XB)=emptyset&elem(XA,s__opens(fX))&elem(XB,s__opens(fX)))). [Info] 00:02.55 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,subseteq(fB,setminus(s__carrier(fX),fA))). [Info] 00:08.11 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,elem(fN,closeds(fX))&elem(fx,fN)&subseteq(fN,fU)). [Info] 00:10.70 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,subseteq(setminus(s__carrier(fX),fA),setminus(s__carrier(fX),setminus(s__carrier(fX),fU)))). [Info] 00:10.98 fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,elem(fN,neighbourhoods(fx,fX))). Verification failed: prover found countermodel fof(eqvilance_teethree_closed_neighbourhood_in_open,conjecture,?[XB,XA]:(elem(fx,XB)&subseteq(fC,XA)&inter(XA,XB)=emptyset&elem(XA,s__opens(fX))&elem(XB,s__opens(fX)))).fof(is_regular,axiom,![XX]:(is_regular(XX)<=>![XV]:![Xp,XC]:((elem(Xp,s__carrier(XX))&~elem(Xp,XC)&elem(XC,closeds(XX)))=>?[XU,XC]:(elem(XU,s__opens(XX))&elem(XC,s__opens(XX))&elem(Xp,XU)&subseteq(XC,XV)&inter(XU,XV)=emptyset)))). fof(eqvilance_teethree_closed_neighbourhood_in_open1,axiom,elem(fx,s__carrier(fX))). fof(eqvilance_teethree_closed_neighbourhood_in_open2,axiom,~elem(fx,fC)). fof(eqvilance_teethree_closed_neighbourhood_in_open3,axiom,elem(fC,closeds(fX))). fof(eqvilance_teethree_closed_neighbourhood_in_open4,axiom,fC=setminus(s__carrier(fX),fU)). fof(eqvilance_teethree_closed_neighbourhood_in_open5,axiom,elem(fx,fU)). fof(eqvilance_teethree_closed_neighbourhood_in_open6,axiom,elem(fU,s__opens(fX))). fof(eqvilance_teethree_closed_neighbourhood_in_open7,axiom,is_regular(fX)&is_kolmogorov(fX)). fof(eqvilance_teethree_closed_neighbourhood_in_open8,axiom,inhabited(fX)). fof(eqvilance_teethree_closed_neighbourhood_in_open9,axiom,topological_space(fX)). real 0m14.914s user 0m37.867s sys 0m1.956s
generated by cgit v1.2.3 (git 2.39.1) at 2025-12-06 14:33:04 +0000