2a:null 2b:["$","title",null,{"children":"Pi-Base tools | danflapjax | Observable"}] 30:T9d0,searched_direct_graph = { let output = ""; for (let entry of search_derivations.direct.entries()) if (!search_derivations.values.has(entry[0]) && !redundant.has(entry[0])) { for (let val of [true,false]) { let descendents = new Map(entry[1].at(val).entries()) descendents.delete(entry[0]); for (let r of redundant) descendents.delete(r) for (let d of entry[1].at(val).entries()) { let grandchildren = search_derivations.direct.get(d[0]).at(d[1].value); for (let r of redundant) grandchildren.delete(r) if (grandchildren.has(entry[0])) continue; //ignore loops for (let g of grandchildren.entries()) { if (g[1].reason !== "given") descendents.delete(g[0]); } } for (let edge of descendents.entries()) { output += `${val?"":"n"}${entry[0]}->${edge[1].value?"":"n"}${edge[0]} [${edge_labels}="${unpad_uid(edge[1].reason)}" URL="https://topology.pi-base.org/theorems/${edge[1].reason}" color="${ spaces_satisfying_search.values().some(space=> space.values.has(entry[0]) && (space.values.get(entry[0]).value != val) && space.values.has(edge[0]) && (space.values.get(edge[0]).value == edge[1].value) )?"DarkGreen": spaces_assuming_search.values().some(space=> space!="contradiction" && space.values.has(entry[0]) && (space.values.get(entry[0]).value != val) && space.values.has(edge[0]) && (space.values.get(edge[0]).value == edge[1].value) )?"GoldenRod":"black" }"];` } } } for (let entry of property_names.entries()) if (!search_derivations.values.has(entry[0]) && !redundant.has(entry[0])){ output += `${entry[0]}[label="${entry[1].replace(/\\/g,"\\\\")}" URL="https://topology.pi-base.org/properties/${entry[0]}" fillcolor="${ spaces_satisfying_search.values().some( space=>space.values.has(entry[0])&&space.values.get(entry[0]).value )?"#bbffbb": spaces_assuming_search.values().some( space=>space!="contradiction"&&space.values.has(entry[0])&&space.values.get(entry[0]).value )?"#ffffaa":"white" }"];n${entry[0]}[label="¬${entry[1].replace(/\\/g,"\\\\")}" URL="https://topology.pi-base.org/properties/${entry[0]}" fillcolor="${ spaces_satisfying_search.values().some( space=>space.values.has(entry[0])&&!space.values.get(entry[0]).value )?"#bbffbb": spaces_assuming_search.values().some( space=>space!="contradiction"&&space.values.has(entry[0])&&!space.values.get(entry[0]).value )?"#ffffaa":"white" }"];` } return output }31:T7c1,selected_property_graph = { let output = ""; for (let entry of search_derivations.direct.get(select[0]).at(value).entries()) if (!redundant.has(entry[0])){ let prop = entry[0]; let val = entry[1].value; let descendents = new Map(search_derivations.direct.get(prop).at(val).entries()) descendents.delete(prop); for (let r of redundant) descendents.delete(r) for (let d of descendents.entries()) { let grandchildren = search_derivations.direct.get(d[0]).at(d[1].value); for (let r of redundant) grandchildren.delete(r) if (grandchildren.has(entry[0])) continue; //ignore loops for (let g of grandchildren.entries()) { if (g[1].reason !== "given") descendents.delete(g[0]); } } for (let edge of descendents.entries()) { output += `${val?"":"n"}${prop}->${edge[1].value?"":"n"}${edge[0]} [${edge_labels}="${edge[1].reason.replace(/([A-Z])0+/g,"$1")}" URL="https://topology.pi-base.org/theorems/${edge[1].reason}" color="${ spaces_satisfying_search.values().some(space=> space.values.has(entry[0]) && (space.values.get(entry[0]).value != val) && space.values.has(edge[0]) && (space.values.get(edge[0]).value == edge[1].value) )?"DarkGreen": spaces_assuming_search.values().some(space=> space!="contradiction" && space.values.has(entry[0]) && (space.values.get(entry[0]).value != val) && space.values.has(edge[0]) && (space.values.get(edge[0]).value == edge[1].value) )?"GoldenRod":"black" }"];` } output += `${val?"":"n"}${prop}[label="${val?"":"¬"}${property_names.get(prop).replace(/\\/g,"\\\\")}" URL="https://topology.pi-base.org/properties/${prop}" fillcolor="${ spaces_satisfying_search.values().some( space=>space.values.has(prop)&&space.values.get(prop).value==val )?"#bbffbb": spaces_assuming_search.values().some( space=>space!="contradiction"&&space.values.has(prop)&&space.values.get(prop).value==val )?"#ffffaa":"white" }"];` } return output }32:T9e1,implications = { let imp = new Map() let cnf = new Map(); //initialize for (let prop of data.properties) { imp.set(prop.uid, [new Map([[prop.uid, {value: false, reason: "given"}]]), new Map([[prop.uid, {value: true, reason: "given"}]])]) } //insert two-term theorems for (let thm of data.theorems) { if (thm.when.kind === "atom") { imp.get(thm.when.property).at(thm.when.value).set(thm.then.property, {value: thm.then.value, reason: thm.uid}) imp.get(thm.then.property).at(!thm.then.value).set(thm.when.property, {value: !thm.when.value, reason: thm.uid}) } else { cnf.set(thm.uid, new Map([...thm.when.subs.map(a => [a.property, !a.value]), [thm.then.property, thm.then.value]])); } } //compute transitive closure of two-term theorems //ideally, should probably be done in topological sort order for efficiency, but this is fine for now for (let antecedent of imp.entries()) { for (let val of [true, false]) { let prop = antecedent[0] let map = antecedent[1].at(val) for (let consequent of map.entries()/*.drop(1)*/) {//.drop(1) skips given let extensions = imp.get(consequent[0]).at(consequent[1].value) for (let extension of extensions.entries()/*.drop(1)*/) { if (!map.has(extension[0])) map.set(extension[0], extension[1]) } } } } //add implications from theorems with three or more terms let changed = new Set(imp.keys()); do { let changed_new = new Set(); for (let thm of cnf.entries()) if (!changed.isDisjointFrom(thm[1])){ let t = [...thm[1].entries()].map(term => imp.get(term[0]).at(term[1])); for (let par of partitions(t)) { let antecedents = intersection(par[0]) if (antecedents.size == 0) continue; let consequents = intersection(par[1]) for (let c of consequents.entries()) { for (let a of antecedents.entries()) { let i = imp.get(a[0]).at(!a[1].value) if (!i.has(c[0])) { i.set(c[0], {value: c[1].value, reason: thm[0]}) changed_new.add(c[0]) } let j = imp.get(c[0]).at(!c[1].value) if (!j.has(a[0])) { j.set(a[0], {value: a[1].value, reason: thm[0]}) changed_new.add(a[0]) } } } } } changed = changed_new } while (changed.size > 0) return {direct: imp, multiterm: cnf}; }33:T1129,function derive(thms, previous = undefined /*for chaining derive*/) { let values, imp, cnf; if (previous) { values = new Map(previous.values) imp = new Map([...previous.direct.entries()].map(a=>[a[0],[new Map(a[1][0]), new Map(a[1][1])]])) cnf = new Map([...previous.multiterm.entries()].map(a=>[a[0], new Map(a[1])])) } else { values = new Map() //deep clones: imp = new Map([...implications.direct.entries()].map(a=>[a[0],[new Map(a[1][0]), new Map(a[1][1])]])) cnf = new Map([...implications.multiterm.entries()].map(a=>[a[0], new Map(a[1])])) } thms = thms.map(thm => new Map(thm)) let changed = new Set(); for (let thm of thms) { const name = [...thm.entries()].map(a=>(a[1]?"":"~")+a[0]).join("|") /*const i = intersection([...thm.entries()].map(term => imp.get(term[0]).at(term[1]))) for (const e of i.entries()) { if (!values.has(e[0])) { values.set(e[0], {value: e[1].value, reason: name}) //imp.delete(e[0]) } else if (values.get(e[0]).value !== e[1].value) { return "contradiction" } } if (thm.size > 1)*/ cnf.set(name, thm) changed = changed.union(thm) } do { let changed_new = new Set(); checkEach: for (let thm of cnf.entries()) if (!changed.isDisjointFrom(thm[1])) { for (let a of thm[1].entries()) { if (values.has(a[0])) { if (values.get(a[0]).value == a[1]) { //theorem is satisfied cnf.delete(thm[0]); continue checkEach; } else { //term cannot be satisfied if (thm[1].size == 1) return "contradiction"//{result: "contradiction", reason: [thm[0], values.get(a[0])]}; thm[1].delete(a[0]) } } else { let contrary = imp.get(a[0]).at(!a[1]) for (let o of thm[1].entries()) if (o[0] != a[0] && contrary.has(o[0])) { if (contrary.get(o[0]).value == o[1]) { //theorem is satisfied regardless of value of a cnf.delete(thm[0]); continue checkEach; } else { //o implies a, so o can be culled from theorem if (thm[1].size == 1) return "contradiction"; thm[1].delete(o[0]) } } } } let t = [...thm[1].entries()].map(term => imp.get(term[0]).at(term[1])); let i = intersection(t) for (let v of i.entries()) { if (!values.has(v[0])) { values.set(v[0], {value: v[1].value, reason: thm[0]}) //imp.delete(v[0]) } else if (values.get(v[0]).value !== v[1].value) { return "contradiction" } changed_new.add(v[0]) } for (let par of partitions(t)) { let antecedents = intersection(par[0]) if (antecedents.size == 0) continue; let consequents = intersection(par[1]) for (let c of consequents.entries()) { for (let a of antecedents.entries()) /*if (!values.has(a[0]) || !values.has(c[0]))*/ { /*if (values.has(a[0]) && !values.has(c[0]) && values.get(a[0]).value == !a[1].value) { values.set(c[0], {value: c[1].value, reason: thm[0]}) } else if (values.has(c[0]) && !values.has(a[0]) && values.get(c[0]).value == !c[1].value) { values.set(a[0], {value: a[1].value, reason: thm[0]}) } else*/ { let i = imp.get(a[0]).at(!a[1].value) if (!i.has(c[0])) { i.set(c[0], {value: c[1].value, reason: thm[0]}) changed_new.add(c[0]) } /*else if (i.get(c[0]).value !== c[1].value) { return "contradiction" }*/ let j = imp.get(c[0]).at(!c[1].value) if (!j.has(a[0])) { j.set(a[0], {value: a[1].value, reason: thm[0]}) changed_new.add(a[0]) } /*else if (j.get(a[0]).value !== a[1].value) { return "contradiction" }*/ } } } } //if (thm[1].size <= 2) cnf.delete(thm[0]) } changed = changed_new } while (changed.size > 0) for (let k of values.keys()) imp.delete(k) for (let e of imp.values()) { for (let k of values.keys()) {e[0].delete(k); e[1].delete(k);} } return {values, direct: imp, multiterm: cnf} }34:[] 2e:{"id":"bb8834d338370a06","slug":"pi-base-tools","title":"Pi-Base tools","thumbnail":"90febf0467040e14ea393867416395e2fc52c9e6e9d580d752a440c3b33251f3","access_level":"unlisted","create_time":"$D2024-08-24T08:12:20.705Z","update_time":"$D2024-11-19T23:01:13.001Z","view_time":null,"first_public_time":null,"has_unpublished_edits":null,"fork":false,"stars":1,"starred":false,"owner":{"type":"team","id":"179dca6cd32ac2a3","login":"dinod123","name":"danflapjax","avatar_url":"https://avatars-next.observableusercontent.com/834271f8dee0f32514ecfb39717000c947f10132d183574179f346e5356cac90","tier":"starter_2024"},"version":1934,"publish_version":null,"role":null,"authored":false,"authors":[{"type":"individual","id":"7c3520bebab3f68f","login":"danflapjax","name":"danflapjax","avatar_url":"https://avatars-next.observableusercontent.com/834271f8dee0f32514ecfb39717000c947f10132d183574179f346e5356cac90","tier":null}],"members":[{"type":"individual","id":"7c3520bebab3f68f","login":"danflapjax","name":"danflapjax","avatar_url":"https://avatars-next.observableusercontent.com/834271f8dee0f32514ecfb39717000c947f10132d183574179f346e5356cac90","tier":null,"role":"editor"},{"type":"team","id":"179dca6cd32ac2a3","login":"dinod123","name":"danflapjax","avatar_url":"https://avatars-next.observableusercontent.com/834271f8dee0f32514ecfb39717000c947f10132d183574179f346e5356cac90","tier":"starter_2024","role":"editor"}],"comments":[],"custom_thumbnail":false,"trashed":false,"lapsed":null,"subscribed":null,"forks":2,"collection":null,"type":"notebook","body":{"titling":"auto","title":"Pi-Base tools","cells":[{"id":0,"value":"# Pi-Base tools","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":1045,"value":"The search is given in [conjunctive normal form](https://en.wikipedia.org/wiki/Conjunctive_normal_form), where each row is a disjunction of terms.","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":123,"value":"viewof search = Inputs.textarea({label: \"Search\", placeholder:\"P164\\n~P78\\nP1 P135\", submit: true})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1331,"value":"tex.options({trust: true})`${\nsearch_cnf.map(thm => [...thm.entries()].map(term => (term[1] ? \"\" : \"\\\\lnot\") + `\\\\href{https://topology.pi-base.org/properties/${term[0]}}{${term[0].replace(/P0+/,\"P\")}}\\\\ \\\\text{${property_names.get(term[0])}}`).join(\"\\\\lor \")).join(\"\\\\land\\\\\\\\ \")\n}`","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1270,"value":"There are **${spaces_satisfying_search.size}** spaces that are known to satisfy the search and a further **${data2.length - spaces_satisfying_search.size}** spaces that might satisfy the search.","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":1406,"value":"| ID | Name | ${properties_in_search.map(p=>`[${property_names.get(p)}](https://topology.pi-base.org/spaces/${p})`).join`|`}\n| - |\n|${search_cnf.length && spaces_assuming_search.entries().filter(e=>e[1]!=\"contradiction\").map(e=>\n [`[${e[0].replace(/S0*/,\"S\")}](https://topology.pi-base.org/spaces/${e[0]})`,\n space_names.get(e[0]),\n ...properties_in_search.map(prop => {\n if (spaces.get(e[0]).values.has(prop)) {\n return spaces.get(e[0]).values.get(prop).value ? \"✅\" : \"❌\"\n } else if (e[1].values.has(prop)) {\n return e[1].values.get(prop).value ? \"❓ (✅)\" : \"❓ (❌)\"\n } else {\n return \"❓\"\n }\n }) \n ].join(\"|\")\n).toArray().join(\"|\\n|\")}","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":1094,"value":"#### Graph styling","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":303,"value":"viewof orientation = Inputs.radio([\"TB\", \"BT\", \"LR\", \"RL\"], {label: \"Orientation\", value: \"TB\"})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":565,"value":"viewof edge_labels = Inputs.radio([\"tooltip\", \"xlabel\", \"label\"], {label: \"Edge labels\", value: \"label\"})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1468,"value":"viewof node_fill = Inputs.toggle({label: \"Color nodes\", value: true})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1043,"value":"### Values implied by search:","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":1824,"value":"viewof quantifiers = Inputs.radio([\"∀∃\", \"∀\", \"∃\"], {value: \"∀∃\", label: \"Quantifiers\"})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1800,"value":"viewof filtered = Inputs.search(\n implied_values.filter(({ quantifier }) => quantifiers.includes(quantifier)),\n { label: \"Property\" }\n)","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1740,"value":"Inputs.table(filtered, {\n columns: [\"quantifier\", \"values\", \"id\", \"name\"],\n format: { id: unpad_uid, name: (n) => tex`\\text{${n}}` },\n align: { quantifier: \"right\" },\n width: { quantifier: 65, values: 70, id: 35 },\n rows: 18.5\n})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1087,"value":"graph(`strict digraph g {\n node [shape=box]\n rankdir = ${orientation};\n ${searched_values_graph}\n}`)","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1277,"value":"The search implies the following sets of properties are equivalent:","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":1705,"value":"viewof extremal = Inputs.toggle({label: \"Only show extremal properties\", value: true})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1286,"value":"tex.options({trust: true})`${\n(extremal ? extremal_equivalence_elements : distinct_equivalences2).map(eq => [...eq.entries()].map(term => (term[1] ? \"\" : \"\\\\lnot\") + `\\\\href{https://topology.pi-base.org/properties/${term[0]}}{${term[0].replace(/P0+/,\"P\")}}\\\\ \\\\text{${property_names.get(term[0])}}`).join(\"\\\\lrArr\")).join(\"\\\\\\\\\\\\text{\\\\textemdash}\\\\\\\\ \")\n}`","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1390,"value":"### Full graph of direct implications\nGreen nodes are ones where a space that satisfies the search and has that property exists in the database, and yellow nodes are ones where a space that may but is not known to satisfy the search would have that property if so. Similarly, green edges are ones where the converse is known to fail for some space, and yellow edges are ones where the converse would fail in a space not known to satisfy the search.","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":978,"value":"graph(`strict digraph g {\n node [style=\"filled\" shape=box]\n //${node_fill ? `node [style=\"filled\"]` : \"\"}\n rankdir = TB;\n ${searched_direct_graph}\n}`)","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1551,"value":"

Further multiterm theorems

\n \n \n \n \n \n \n \n \n ${search_derivations.multiterm.entries().map(a=>\n html`\n ${tex.options({trust: true})`${\na[1].entries().map(term => (term[1] ? \"\" : \"\\\\lnot\") + `\\\\href{https://topology.pi-base.org/properties/${term[0]}}{${term[0].replace(/P0+/,\"P\")}}\\\\ \\\\text{${property_names.get(term[0])}}`).toArray().join(\"\\\\lor \")}`}\n `//...a[1].entries()]`\n ).toArray()}\n \n

ID	Theorem
${unpad_uid(a[0])}

","pinned":false,"hidden":false,"mode":"html","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":1404,"value":"Select subgraph of properties implied by a chosen property:","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":340,"value":"viewof prop = Inputs.search(data.properties.map(p => [p.uid, p.name, ...p.aliases]).filter(p => search_derivations.direct.has(p[0])), {label: \"Property\"/*, query: \"T6\"*/})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":367,"value":"viewof select = Inputs.select(prop)","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1313,"value":"tex.options({trust: true})`${\n[...(new Map(equivalences)).get(select[0]).entries()].map(term => (term[1].value ? \"\" : \"\\\\lnot\") + `\\\\href{https://topology.pi-base.org/properties/${term[0]}}{${term[0].replace(/P0+/,\"P\")}}\\\\ \\\\text{${property_names.get(term[0])}}`).join(\"\\\\lrArr\")\n}`","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":332,"value":"viewof value = Inputs.radio([true, false], {label: \"Value\", value: true})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":288,"value":"graph(`strict digraph g {\n node [shape=box style=\"filled\"]\n//${node_fill ? `node [style=\"filled\"]` : \"\"}\n rankdir = ${orientation};\n ${selected_property_graph}\n}`)","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1603,"value":"View properties of spaces under the assumption that they satisfy the search:","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":1506,"value":"viewof space_search = Inputs.search(data.spaces.map(s => [s.uid, s.name, ...s.aliases])\n .filter(s => spaces_assuming_search.get(s[0]) != \"contradiction\"), {label: \"Space\"})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1510,"value":"viewof space_select = Inputs.select(space_search)","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1522,"value":"selected_space_values","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":764,"value":"viewof branch = Inputs.text({label: \"Branch\", value: \"main\", submit: true})","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1481,"value":"* **Spaces**: ${data.spaces.length}\n* **Properties**: ${data.properties.length}\n* **Theorems**: ${data.theorems.length}\n* **Traits**: ${[...spaces.values()].reduce((a,c)=>a+c.values.size,0)}\n* **Multiterm theorems**: ${implications.multiterm.size}\n* **Direct implications**: ${implications.direct.values().reduce((a,c)=>a+c[0].size,0)}","pinned":false,"hidden":false,"mode":"md","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"","database":"$undefined"},{"id":891,"value":"search_derivations=derive(search_cnf)","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1639,"value":"implied_values = property_names.entries().map(([id, name]) => {\n if (search_derivations.values.has(id)) return {quantifier: \"∀\", values: search_derivations.values.get(id).value ? \"✅\" : \"❌\", id, name}\n if (spaces_satisfying_search.size == 0) return {quantifier: \"∃\", values: \"❓\", id, name}\n return {quantifier: \"∃\", id, name,\n values: (spaces_satisfying_search.values().some(v => v.values.has(id) && v.values.get(id).value) ? \"✅\" : \"\")\n + (spaces_satisfying_search.values().some(v => v.values.has(id) && !v.values.get(id).value) ? \"❌\" : \"\")\n + (spaces_satisfying_search.values().some(v => !v.values.has(id)) ? \"❓\" : \"\")}\n}).toArray()","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1050,"value":"equivalences = {\n return [...search_derivations.direct.entries()].map(a => [a[0], intersection_negation(a[1])])\n\n function intersection_negation(list) {\n let [f, t] = list\n let i = new Map(t)\n for (let e of i.entries()) { \n if (!f.has(e[0]) || f.get(e[0]).value == e[1].value) i.delete(e[0])\n }\n return i\n }\n}","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1009,"value":"searched_values_graph = {\n let output = \"\";\n for (let entry of search_derivations.values.entries()) {\n let prop = entry[0]; let val = entry[1].value;\n let descendents = new Map(implications.direct.get(prop).at(val).entries())\n descendents.delete(prop);\n for (let d of descendents.entries()) {\n let grandchildren = implications.direct.get(d[0]).at(d[1].value);\n if (grandchildren.has(entry[0])) continue; //ignore loops\n for (let g of grandchildren.entries()) {\n if (g[1].reason !== \"given\") descendents.delete(g[0]);\n }\n }\n for (let edge of descendents.entries()) {\n output += `${val?\"\":\"n\"}${prop}->${edge[1].value?\"\":\"n\"}${edge[0]} [${edge_labels}=${edge[1].reason.replace(/T0*/,\"T\")} URL=\"https://topology.pi-base.org/theorems/${edge[1].reason}\"];`\n }\n output += `${val?\"\":\"n\"}${prop}[label=\"${val?\"\":\"¬\"}${property_names.get(prop)}\" URL=\"https://topology.pi-base.org/properties/${prop}\"];`\n }\n \n return output\n}","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1130,"value":"distinct_equivalences = {\n let d = new Map()\n let seen = new Set()\n for (let eq of equivalences) if (!seen.has(eq[0]) && eq[1].size > 1) {\n let [first, ...rest] = [...eq[1].entries()]\n d.set(first[0], new Map(rest.sort().map(a=>[a[0], a[1].value])))\n seen = seen.union(eq[1])\n }\n return d\n}","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1166,"value":"distinct_equivalences2 = {\n let d = []\n let seen = new Set()\n for (let eq of equivalences) if (!seen.has(eq[0]) && eq[1].size > 1) {\n d.push(new Map([...eq[1].entries()]\n .map(a=>{let d=implications.direct.get(a[0]); return [...a,d[0].size+d[1].size]})\n .sort(/*(a,b)=>b[2]-a[2]*/).map(a=>[a[0], a[1].value])))\n seen = seen.union(eq[1])\n }\n return d\n}","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1150,"value":"redundant = distinct_equivalences2.values().map(a=>new Set(a.keys().drop(1)))\n .reduce((a,c)=>a.union(c),new Set())\n //distinct_equivalences.values().reduce((a,c)=>a.union(c),new Set())","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1687,"value":"extremal_equivalence_elements = distinct_equivalences2.map(m => {let s = new Set(m.keys());\n s.delete(\"P000071\"); //stupid hack\n return new Map(m.entries().filter(p => s.intersection(implications.direct.get(p[0])[0]).size == 1 || s.intersection(implications.direct.get(p[0])[1]).size == 1))})","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":967,"value":"search_derivations.direct.values().reduce((a,c)=>a+c[0].size,0)","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":976,"value":"$30","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":280,"value":"$31","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":153,"value":"$32","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":461,"value":"function intersection(list) {\n let [least, ...rest] = list.toSorted((a,b) => a.size - b.size)\n let i = new Map(least)\n for (let r of rest) {\n for (let e of i.entries()) { \n if (!r.has(e[0]) || r.get(e[0]).value !== e[1].value) i.delete(e[0])\n }\n }\n return i\n}","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":593,"value":"function* partitions(list, index=1) {\n const max = 2**(list.length-1)\n for (let sel = index; sel < max; sel++) {\n let o = [[],[]]\n for (let i = 0; i < list.length; i++) o[(sel>>i)&1].push(list[i])\n yield o;\n }\n}","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":777,"value":"$33","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":920,"value":"function* graph(g) {\n const svg = dot`${g}`;\n const s = d3.select(svg)\n const zoom = d3.zoom()\n .scaleExtent([0.9, 50])\n .on(\"zoom\", zoomed)\n s.call(zoom)\n \n zoom.translateBy(s, ...(a=>[parseFloat(a[1]),parseFloat(a[2])])(s.select(\"#graph0\").attr(\"transform\").match(/translate\$(.*) (.*)\$/)))\n const start = d3.zoomTransform(svg)\n\n s.attr(\"height\", s.attr(\"width\"))\n\n function zoomed({ transform }) {\n s.select(\"#graph0\").attr(\"transform\", transform);\n }\n\n function reset() {\n s.transition()\n .duration(500)\n .call(zoom.transform, start);\n } \n\n const div = document.createElement(\"div\");\n div.append(svg)\n const button = Inputs.button(\"Reset zoom\", {reduce: reset});\n div.prepend(button);\n \n yield div\n}","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":207,"value":"property_names = new Map(data.properties.map(p => [p.uid, p.name]))","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1428,"value":"space_names = new Map(data.spaces.map(p => [p.uid, p.name]))","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1200,"value":"spaces_assuming_search = new Map(spaces.entries().map(s => [s[0],derive(search_cnf,s[1])]))","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1255,"value":"spaces_satisfying_search = new Map(spaces.entries().filter(s => search_cnf.reduce((a,c) => a && c.entries().reduce((a2,c2)=> a2 || (s[1].values.has(c2[0]) && s[1].values.get(c2[0]).value == c2[1]),false), true)))","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1208,"value":"data2 = [...spaces_assuming_search.entries()].filter(s => s[1] !== \"contradiction\").map(s => s[1].values.entries().reduce((a,c)=>(a[c[0]]=c[1], a), {name: s[0]}))","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1098,"value":"spaces = new Map(data.spaces.map(s=>[s.uid,derive(data.traits.filter(t=>t.space == s.uid).map(t=>new Map([[t.property, t.value]])))]))","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1108,"value":"[...spaces.values()].reduce((a,c)=>a+c.values.size,0)","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":4,"value":"data = fetch(`https://pi-base-bundles.s3.us-east-2.amazonaws.com/refs/heads/${branch}.json`).then(response => response.json());","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1566,"value":"function unpad_uid(text) {\n return text.replace(/([A-Z])0+/gi,\"$1\")\n}","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":815,"value":"search_cnf = search.split(\"\\n\").filter(a=>!/^\\s*$/.test(a)).map(s => new Map(s.trim().split(/\\s+/gi).map(s => [\"P\"+s.match(/\\d+/)[0].padStart(6,\"0\"), /p|\\d/i.test(s[0])])))","pinned":false,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1411,"value":"properties_in_search = search_cnf.reduce((a,c)=>a.union(c),new Set()).values().toArray()","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"},{"id":1515,"value":"selected_space_values = [...spaces_assuming_search.get(space_select[0]).values]","pinned":true,"hidden":false,"mode":"ojs","author":"$undefined","summary":"$undefined","providerMetadata":"$undefined","attachments":"$undefined","output":"$undefined","database":"$undefined"}],"files":"$W34","stdlib":"1"}} 2f:"$2e:body"