• Daniel Donnelly, Jr. (24/24) Nov 17 2022 The following code is non-functional, just a sketch:

Daniel Donnelly, Jr. <enjoysmath gmail.com> writes:

The following code is non-functional, just a sketch:

```
    class Subgroup : Definition
    {
    public:
       Set G;
       Set H;

    private:
       Assert[] given = [G in Grp("G"), H=subset(G, "H")];
       Assert[] input = [[a,b] in H >>> a*(b^(-1)) in H]];
       Assert[] output = [H ~ " is a subgroup of " ~ G];
       Notate[] denoted = [H ~ r"\leqslant " ~ G];
    }
```

There will be a gigantic brain-like graph.  Nodes with I/O.  For 
each new Definition/Assertion made by the user, I would like them 
to be automatically wired-into the brain graph up to variable 
substitution.  So it's not as simple as using an AA to accomplish 
this.  And I don't want to loop through all nodes and then check 
for all outputs that match the inputs, etc.  So can you think of 
a way to accomplish this, especially that is D-friendly?

Up to variable substitution means there is a mechanism that knows 
that "A is a subgroup of B" is essentially the same thing as "H 
is a subgroup of G", you simply map the variables appropriately.