summaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Collapse)Author
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-24First atemped to write a new way of local function defintionSimon-Kor
2024-08-24naproch sty extensionSimon-Kor
2024-08-14some wishes for NaprocheZFSimon-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-09fixed axiomatic errorSimon-Kor
2024-08-09put cardinalit to the right placeSimon-Kor
2024-08-07Created first urysohn formalizationSimon-Kor
2024-07-21Further Formalisation on numbersSimon-Kor
2024-07-06Formalisation of rationals.Simon-Kor
2024-07-06Formalisation of integers.Simon-Kor
2024-07-06Finished the formalization of naturals.Simon-Kor
2024-07-05Proof of 1 is identity on the naturals and beginSimon-Kor
of Disstributiv law naturals proof
2024-07-02Further Formalisation of naturals.Simon-Kor
Such as induction on naturals and addition laws.
2024-07-02Definition and axioms of naturals.Simon-Kor
2024-06-26Merge remote-tracking branch 'upstream/main' into formalisation_numbersSimon-Kor
2024-06-26Working at the numbers.texSimon-Kor
2024-06-25Update equivalence.texadelon
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-25Improvement for the ATP proof timeSimon-Kor
2024-06-25Sorted the structure of numbers.texSimon-Kor
2024-06-25definition of equivalence_from_partition can proof false in everything.texSimon-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
2024-06-18Merge remote-tracking branch 'upstream/main'Simon-Kor
2024-06-18Definition of T3 and regular spaces.Simon-Kor
2024-06-18Update topological-space.texadelon
2024-06-17Completed proofs [stable]Simon-Kor
2024-06-16First implementation of basic relations of closed and open.Simon-Kor
Not finished.
2024-06-12Prove Bug "Ex falso quodlibet"Simon-Kor
The generated ATP Tasks are done in few secounds, if they are send manually to Vampire. But if its done in Naproche all together it won't work.
2024-06-11proof of complement_interior_eq_closure_complement and some more about ↵Simon-Kor
clousures(unsatable)
2024-06-04Proof of teetwo_space_is_teeone_spaceSimon-Kor
2024-06-04Proof of teeone_implies_singletons_closedSimon-Kor
The Assumption was changed, for usage of bounded variables. Maybe there is a bug with Omitted. Omitted restricts the Ambigus Phrase testing.
2024-06-04Some notation fixes and lemma for topo basis generats opens was proofed and ↵Simon-Kor
optimizised
2024-05-28Merge branch 'main' into mainSimon-Kor
2024-05-28unexpected behavior of vampireSimon-Kor
The task topological behavior is proofed in seconds by just vampire, but with mode casc it takes plenty seconds
generated by cgit v1.2.3 (git 2.39.1) at 2025-12-06 10:06:26 +0000