| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2024-09-03 | Finished induction begin | Simon-Kor | |
| 2024-09-02 | working commit | Simon-Kor | |
| 2024-09-02 | working commit | Simon-Kor | |
| 2024-09-02 | Corrected Contradiction. | Simon-Kor | |
| Contradiction was due to a misstake in the definition in sequence. | |||
| 2024-08-31 | Contradiction in sequence | Simon-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-31 | working commit | Simon-Kor | |
| 2024-08-30 | working commit | Simon-Kor | |
| 2024-08-29 | working commit | Simon-Kor | |
| 2024-08-28 | working commit | Simon-Kor | |
| 2024-08-27 | working commit | Simon-Kor | |
| 2024-08-27 | Feature Complete | Simon-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-27 | ambigus parse fix. The proof goal must be changed, | Simon-Kor | |
| since now some could define a function with overlapping and worng subdomains | |||
| 2024-08-27 | Experimental working commit, programm will compile | Simon-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-24 | naproch sty extension | Simon-Kor | |
| 2024-08-14 | The added proposition and definition should have | Simon-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-13 | less urysohn | Simon-Kor | |
| 2024-08-12 | way way way way more urysohn | Simon-Kor | |
| 2024-08-12 | way way way more urysohn | Simon-Kor | |
| 2024-08-12 | way way more urysohn | Simon-Kor | |
| 2024-08-12 | way more urysohn | Simon-Kor | |
| 2024-08-12 | Completed the structure of the proof of Urysohn. | Simon-Kor | |
| Now every single step has to be proven. | |||
| 2024-08-12 | more more way more urysohn | Simon-Kor | |
| 2024-08-11 | more more more urysohn | Simon-Kor | |
| 2024-08-10 | more more urysohn | Simon-Kor | |
| 2024-08-10 | more urysohn | Simon-Kor | |
| 2024-08-10 | more ur<sohn | Simon-Kor | |
| 2024-08-09 | put cardinalit to the right place | Simon-Kor | |
| 2024-08-07 | Created first urysohn formalization | Simon-Kor | |
| 2024-06-25 | [Stable] Implented continuous.tex and omitted some proves | Simon-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-25 | Improvement for the ATP proof time | Simon-Kor | |
| 2024-06-20 | [Stable] Topologgical-space.tex | Simon-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-18 | Merge remote-tracking branch 'upstream/main' | Simon-Kor | |
| 2024-06-18 | Definition of T3 and regular spaces. | Simon-Kor | |
| 2024-06-18 | Update topological-space.tex | adelon | |
| 2024-06-17 | Completed proofs [stable] | Simon-Kor | |
| 2024-06-16 | First implementation of basic relations of closed and open. | Simon-Kor | |
| Not finished. | |||
| 2024-06-12 | Prove 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-11 | proof of complement_interior_eq_closure_complement and some more about ↵ | Simon-Kor | |
| clousures(unsatable) | |||
| 2024-06-04 | Proof of teetwo_space_is_teeone_space | Simon-Kor | |
| 2024-06-04 | Proof of teeone_implies_singletons_closed | Simon-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-04 | Some notation fixes and lemma for topo basis generats opens was proofed and ↵ | Simon-Kor | |
| optimizised | |||
| 2024-05-28 | Merge branch 'main' into main | Simon-Kor | |
| 2024-05-28 | unexpected behavior of vampire | Simon-Kor | |
| The task topological behavior is proofed in seconds by just vampire, but with mode casc it takes plenty seconds | |||
| 2024-05-28 | Update `inters_in_genopens` | adelon | |
| 2024-05-28 | Merge branch 'main' into main | Simon-Kor | |
| 2024-05-28 | proofing some lammes about topological basis | Simon-Kor | |
| 2024-05-25 | Prove `emptyset_open` to replace structure axiom | adelon | |
| 2024-05-22 | Update label for `genopens` | adelon | |
| 2024-05-21 | Allow line breaks via `\textbox`, handle `\left`/`\right` | adelon | |
 |
index : naproche-zf.git | |
| Unnamed repository; edit this file 'description' to name the repository. |
| summaryrefslogtreecommitdiff |