Fact.cs

            return true;

        CircleFact c1f1 = (CircleFact)_Facts[f1.Cid1];
        CircleFact c1f2 = (CircleFact)_Facts[f2.Cid1];

        PointFact p1f1 = (PointFact)_Facts[f1.Pid1];
        PointFact p1f2 = (PointFact)_Facts[f2.Pid1];

        return (c1f1.Equivalent(c1f2)&& p1f1.Equivalent(p1f2) && (Mathf.Abs(f1.vol - f2.vol) < 0.001) );
        
    }
}

/// <summary>
/// The fact that the plane of a <see cref="CircleFact">CircleFact</see> and the line <see cref="RayFact>RayFact</see> are orthogonal
/// </summary>
public class OrthogonalCircleLineFact : FactWrappedCRTP<OrthogonalCircleLineFact>
{
    /// \copydoc Fact.s_type
    [JsonProperty]
    protected static new string s_type = "OrthogonalCircleLineFact";

    ///  <summary> a <see cref="CircleFact">CircleFact</see> describing the base area </summary>
    public string Cid1;
    ///  <summary> a <see cref="RayFact">Rayfact</see> describing the line </summary>
    public string Lid1;
  

    /// <summary> \copydoc Fact.Fact </summary>
    public OrthogonalCircleLineFact() : base()
    {
        this.Cid1 = null;
        this.Lid1 = null;

    }

    /// <summary>
    /// Copies <paramref name="fact"/> by initiating new MMT %Fact.
    /// </summary>
    /// <param name="fact">Fact to be copied</param>
    /// <param name="old_to_new"><c>Dictionary</c> mapping <paramref name="fact"/>.<see cref="getDependentFactIds"/> in <paramref name="fact"/>.<see cref="Fact._Facts"/> to corresponding <see cref="Fact.Id"/> in <paramref name="organizer"/> </param>
    /// <param name="organizer">sets <see cref="_Facts"/></param>
    public OrthogonalCircleLineFact(OrthogonalCircleLineFact fact, Dictionary<string, string> old_to_new, FactOrganizer organizer) : base(fact, organizer)
    {
        init(old_to_new[fact.Cid1], old_to_new[fact.Lid1]);
    }

    /// <summary>
    /// Standard Constructor
    /// </summary>
    /// <param name="cid1">sets <see cref="Cid1"/></param>
    /// <param name="lid1">sets <see cref="Lid1"/></param>
    /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    public OrthogonalCircleLineFact(string cid1, string lid1, FactOrganizer organizer) : base(organizer)
    {
        init(cid1, lid1);
    }

    /// <summary>
    /// Initiates <see cref="Pid1"/>, <see cref="Pid2"/>, <see cref="Pid3"/>, <see cref="is_right_angle"/>, <see cref="Fact._URI"/> and creates MMT %Fact Server-Side
    /// </summary>
    /// <param name="cid1">sets <see cref="Cid1"/></param>
    /// <param name="lid1">sets <see cref="Lid1"/></param>
    private void init(string cid1, string lid1)
    {
        this.Cid1 = cid1;
        this.Lid1 = lid1;

        CircleFact cf1 = _Facts[cid1] as CircleFact;
        RayFact lf1 = _Facts[lid1] as RayFact;


        MMTDeclaration mmtDecl;
        string c1URI = cf1.Id;
        string l1URI = lf1.Id;


        mmtDecl = generateMMTDeclaration(c1URI, l1URI);

        AddFactResponse.sendAdd(mmtDecl, out this._URI);
    }

    /// <summary>
    /// Bypasses initialization of new MMT %Fact by using existend URI, _which is not checked for existence_.
    /// </summary>
    /// <param name="Cid1">sets <see cref="Cid1"/></param>
    /// <param name="Lid1">sets <see cref="Lid1"/></param>
    /// <param name="backendURI">MMT URI</param>
    /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    public OrthogonalCircleLineFact(string Cid1, string Lid1,  string backendURI, FactOrganizer organizer) : base(organizer)
    {
        this.Cid1 = Cid1;
        this.Lid1 = Lid1;

        this._URI = backendURI;
        _ = this.Label;
    }

    /// \copydoc Fact.parseFact(Scroll.ScrollFact)
    public new static OrthogonalCircleLineFact parseFact(Scroll.ScrollFact fact)
    {
        OMA tp = (OMA)((Scroll.ScrollSymbolFact)fact).tp;
        if (tp == null)
            return null;

        string uri = fact.@ref.uri;

        string CircleUri = ((OMS)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[0]).uri;
        string LineUri = ((OMS)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[1]).uri;

        if (StageStatic.stage.factState.ContainsKey(CircleUri)
         && StageStatic.stage.factState.ContainsKey(LineUri))

            return new OrthogonalCircleLineFact(CircleUri, LineUri, uri, StageStatic.stage.factState);

        else    //If dependent facts do not exist return null
            return null;
    }

    /// \copydoc Fact.generateLabel
    protected override string generateLabel()
    {
        return   _Facts[Cid1].Label + "⊥" + _Facts[Lid1].Label;
    }

    /// <summary>
    /// Constructs struct for not-right-angled MMT %Fact <see cref="AddFactResponse"/>
    /// </summary>
    /// <param name="c1URI"> Uri for <see cref="Cid1"/></param>
    /// <param name="l1URI"> Uri for <see cref="Lid1"/></param>
    /// <returns>struct for <see cref="AddFactResponse"/></returns>
    private MMTDeclaration generateMMTDeclaration(string c1URI, string l1URI)
    {
        List<MMTTerm> innerArguments = new List<MMTTerm>
        {
            new OMS(c1URI),
            new OMS(l1URI)
        };

        List<MMTTerm> outerArguments = new List<MMTTerm>
        {
            new OMA(new OMS(MMTURIs.OrthoCircleLine), innerArguments)
        };
        MMTTerm tp = new OMA(new OMS(MMTURIs.Ded), outerArguments);
        MMTTerm df = null;

        return new MMTSymbolDeclaration(this.Label, tp, df);
    }

    /// \copydoc Fact.hasDependentFacts
    public override Boolean hasDependentFacts()
    {
        return true;
    }

    /// \copydoc Fact.getDependentFactIds
    public override string[] getDependentFactIds()
    {
        return new string[] { Cid1, Lid1 };
    }

    /// \copydoc Fact.instantiateDisplay(GameObject, Transform)
    public override GameObject instantiateDisplay(GameObject prefab, Transform transform)
    {
        var obj = GameObject.Instantiate(prefab, Vector3.zero, Quaternion.identity, transform);
        obj.transform.GetChild(0).gameObject.GetComponent<TextMeshProUGUI>().text = _Facts[this.Cid1].Label;
        obj.transform.GetChild(1).gameObject.GetComponent<TextMeshProUGUI>().text = _Facts[this.Lid1].Label;

        obj.GetComponent<FactWrapper>().fact = this;
        return obj;
    }

    /// \copydoc Fact.GetHashCode
    /// uhhh is this a problem?
    public override int GetHashCode()
    {
        return this.Cid1.GetHashCode() ^ this.Lid1.GetHashCode();
    }

    /// \copydoc Fact.Equivalent(Fact, Fact)
    protected override bool EquivalentWrapped(OrthogonalCircleLineFact f1, OrthogonalCircleLineFact f2)
    {
        if (f1.Cid1 == f2.Cid1 && f1.Lid1 == f2.Lid1)
            return true;

        CircleFact c1f1 = (CircleFact)_Facts[f1.Cid1];
        CircleFact c1f2 = (CircleFact)_Facts[f2.Cid1];

        RayFact l1f1 = (RayFact)_Facts[f1.Lid1];
        RayFact l1f2 = (RayFact)_Facts[f2.Lid1];

        return (c1f1.Equivalent(c1f2) && l1f1.Equivalent(l1f2));

    }
}

/// <summary>
/// The volume of a cone A  defined by a base area  <see cref="CircleFact">CircleFact</see>, a top area <see cref="CircleFact">CircleFact</see> and the volume as float
/// </summary>
public class TruncatedConeVolumeFact : FactWrappedCRTP<TruncatedConeVolumeFact>
{
    /// \copydoc Fact.s_type
    [JsonProperty]
    protected static new string s_type = "TruncatedConeVolumeFact";

    ///  <summary> a <see cref="CircleFact">CircleFact</see> describing the base area </summary>
    public string Cid1;
    ///  <summary> a <see cref="CircleFact">CircleFact</see> describing the top area  </summary>
    public string Cid2;
    ///  <summary> the volume of Truncated the cone as a float </summary>
    public float vol;
    /// <summary> a proof that both circles have not the same size </summary>
    public string unequalCirclesProof;
    ///  <summary> OMA proof that the two circles are parallel  </summary>
    public OMA proof;
    

    /// <summary> \copydoc Fact.Fact </summary>
    public TruncatedConeVolumeFact() : base()
    {
        this.Cid1 = null;
        this.Cid2 = null;
        this.vol = 0.0f;
        this.unequalCirclesProof = null;
        this.proof = null;

    }

    /// <summary>
    /// Copies <paramref name="fact"/> by initiating new MMT %Fact.
    /// </summary>
    /// <param name="fact">Fact to be copied</param>
    /// <param name="old_to_new"><c>Dictionary</c> mapping <paramref name="fact"/>.<see cref="getDependentFactIds"/> in <paramref name="fact"/>.<see cref="Fact._Facts"/> to corresponding <see cref="Fact.Id"/> in <paramref name="organizer"/> </param>
    /// <param name="organizer">sets <see cref="_Facts"/></param>
    public TruncatedConeVolumeFact(TruncatedConeVolumeFact fact, Dictionary<string, string> old_to_new, FactOrganizer organizer) : base(fact, organizer)
    {
        init(old_to_new[fact.Cid1], old_to_new[fact.Cid2], fact.vol, old_to_new[fact.unequalCirclesProof], fact.proof);
    }

    /// <summary>
    /// Standard Constructor
    /// </summary>
    /// <param name="cid1">sets <see cref="Cid1"/></param>
    /// <param name="cid2">sets <see cref="Cid2"/></param>
    /// <param name="vol">sets <see cref="vol"/></param>
    /// <param name="proof">sets <see cref="proof"/></param>
    /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    public TruncatedConeVolumeFact(string cid1, string cid2, float vol, string unequalproof, OMA proof, FactOrganizer organizer) : base(organizer)
    {
        init(cid1, cid2, vol,unequalproof, proof);
    }

    /// <summary>
    /// sets variables and generates MMT Declaration
    /// </summary>
    /// <param name="cid1">sets <see cref="Cid1"/></param>
    /// <param name="cid2">sets <see cref="Cid2"/></param>
    /// <param name="vol">sets <see cref="vol"/></param>
    /// <param name="proof">sets <see cref="proof"/></param>
    private void init(string cid1, string cid2, float vol, string unequalproof, OMA proof)
    {
        this.Cid1 = cid1;
        this.Cid2 = cid2;
        this.proof = proof;
        this.unequalCirclesProof = unequalproof;

        CircleFact cf1 = _Facts[cid1] as CircleFact;
        CircleFact cf2 = _Facts[cid2] as CircleFact;
        this.vol = vol;
        UnEqualCirclesFact unEqualProof = _Facts[unequalproof] as UnEqualCirclesFact;

        MMTDeclaration mmtDecl;
        string c1URI = cf1.Id;
        string c2URI = cf2.Id;
        string pURI = unEqualProof.Id;

        mmtDecl = generateMMTDeclaration(c1URI, c2URI, vol, pURI, proof);

        AddFactResponse.sendAdd(mmtDecl, out this._URI);
    }

    /// <summary>
    /// Bypasses initialization of new MMT %Fact by using existend URI, _which is not checked for existence_.
    /// </summary>
    /// <param name="Cid1">sets <see cref="Cid1"/></param>
    /// <param name="Cid2">sets <see cref="Cid2"/></param>
    /// <param name="volume">sets <see cref="vol"/></param>
    /// <param name="proof">sets <see cref="proof"/></param>
    /// <param name="backendURI">MMT URI</param>
    /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    public TruncatedConeVolumeFact(string Cid1, string Cid2, float volume, string unequalproof, OMA proof, string backendURI, FactOrganizer organizer) : base(organizer)
    {
        this.Cid1 = Cid1;
        this.Cid2 = Cid2;
        this.vol = volume;
        this.proof = proof;
        this.unequalCirclesProof = unequalproof;

        this._URI = backendURI;
        _ = this.Label;
    }

    /// \copydoc Fact.parseFact(Scroll.ScrollFact)
    public new static TruncatedConeVolumeFact parseFact(Scroll.ScrollFact fact)
    {
        string uri = fact.@ref.uri;

        string Circle1Uri = ((OMS)((OMA)((OMA)((Scroll.ScrollValueFact)fact).lhs).arguments[0]).arguments[0]).uri;
        string Circle2Uri = ((OMS)((OMA)((OMA)((Scroll.ScrollValueFact)fact).lhs).arguments[0]).arguments[1]).uri;
        float volume = ((OMF)((Scroll.ScrollValueFact)fact).value).f;

        string UnEqualCirclesProof = ((OMS)(((OMA)((OMA)((Scroll.ScrollValueFact)fact).lhs).arguments[0]).arguments[2])).uri;
        OMA proof = (OMA)(((OMA)((OMA)((Scroll.ScrollValueFact)fact).lhs).arguments[0]).arguments[3]);


        if (StageStatic.stage.factState.ContainsKey(Circle1Uri) && StageStatic.stage.factState.ContainsKey(Circle2Uri))

            return new TruncatedConeVolumeFact(Circle1Uri, Circle2Uri, volume, UnEqualCirclesProof , proof, uri,  StageStatic.stage.factState);

        else    //If dependent facts do not exist return null
            return null;
    }

    /// \copydoc Fact.generateLabel
    protected override string generateLabel()
    {
        return "V(" + _Facts[Cid1].Label +"," + _Facts[Cid2].Label+")";
    }



    /// <summary>
    /// Constructs struct for not-right-angled MMT %Fact <see cref="AddFactResponse"/>
    /// </summary>
    /// <param name="c1URI"> Uri for <see cref="Cid1"/></param>
    /// <param name="c2URI"> Uri for <see cref="Cid2"/></param>
    /// <param name="val"> <see cref="vol"/></param>
    /// <returns>struct for <see cref="AddFactResponse"/></returns>
    private MMTDeclaration generateMMTDeclaration(string c1URI, string c2URI, float val, string unequalproof, OMA proof)
    {
        MMTTerm lhs =
            new OMA(
                new OMS(MMTURIs.TruncatedVolumeCone),

                new List<MMTTerm> {
                    new OMS(c1URI),
                    new OMS(c2URI),
                    new OMS(unequalproof),
                    proof,
                }
            );

        MMTTerm valueTp = new OMS(MMTURIs.RealLit);
        MMTTerm value = new OMF(val);

        return new MMTValueDeclaration(this.Label, lhs, valueTp, value);
    }

    /// \copydoc Fact.hasDependentFacts
    public override Boolean hasDependentFacts()
    {
        return true;
    }

    /// \copydoc Fact.getDependentFactIds
    public override string[] getDependentFactIds()
    {
        return new string[] { Cid1, Cid2 };
    }

    /// \copydoc Fact.instantiateDisplay(GameObject, Transform)
    public override GameObject instantiateDisplay(GameObject prefab, Transform transform)
    {
        var obj = GameObject.Instantiate(prefab, Vector3.zero, Quaternion.identity, transform);
        obj.transform.GetChild(0).gameObject.GetComponent<TextMeshProUGUI>().text = _Facts[this.Cid1].Label + _Facts[this.Cid2].Label;
        obj.GetComponent<FactWrapper>().fact = this;

        return obj;
    }

    /// \copydoc Fact.GetHashCode
    /// uhhh is this a problem?
    public override int GetHashCode()
    {
        return this.Cid1.GetHashCode() ^ this.Cid2.GetHashCode();
    }

    /// \copydoc Fact.Equivalent(Fact, Fact)
    protected override bool EquivalentWrapped(TruncatedConeVolumeFact f1, TruncatedConeVolumeFact f2)
    {
        if (f1.Cid1 == f2.Cid1 && f1.Cid2 == f2.Cid2)
            return true;

        CircleFact c1f1 = (CircleFact)_Facts[f1.Cid1];
        CircleFact c1f2 = (CircleFact)_Facts[f2.Cid1];

        CircleFact c2f1 = (CircleFact)_Facts[f1.Cid2];
        CircleFact c2f2 = (CircleFact)_Facts[f2.Cid2];

        return (c1f1.Equivalent(c1f2) && c2f1.Equivalent(c2f2) && (Mathf.Abs(f1.vol - f2.vol) < 0.001) );

    }
}

/// <summary>
/// The volume of a cylinder defined by a base area  <see cref="CircleFact">CircleFact</see>, a top area <see cref="CircleFact">CircleFact</see> and the volume as float
/// </summary>
public class CylinderVolumeFact : FactWrappedCRTP<CylinderVolumeFact>
{
    /// \copydoc Fact.s_type
    [JsonProperty]
    protected static new string s_type = "CylinderVolumeFact";

    ///  <summary> a <see cref="CircleFact">CircleFact</see> describing the base area </summary>
    public string Cid1;
    ///  <summary> a <see cref="CircleFact">CircleFact</see> describing the top area  </summary>
    public string Cid2;
    ///  <summary> the volume of the cylinder as a float </summary>
    public float vol;
    /// <summary> a proof that both circles have the same size </summary>
    public string equalCirclesProof;
    ///  <summary> OMA proof that the two circles are parallel  </summary>
    public OMA proof;

    /// <summary> \copydoc Fact.Fact </summary>
    public CylinderVolumeFact() : base()
    {
        this.Cid1 = null;
        this.Cid2 = null;
        this.vol = 0.0f;
        this.proof = null;
        this.equalCirclesProof = null;

    }

    /// <summary>
    /// Copies <paramref name="fact"/> by initiating new MMT %Fact.
    /// </summary>
    /// <param name="fact">Fact to be copied</param>
    /// <param name="old_to_new"><c>Dictionary</c> mapping <paramref name="fact"/>.<see cref="getDependentFactIds"/> in <paramref name="fact"/>.<see cref="Fact._Facts"/> to corresponding <see cref="Fact.Id"/> in <paramref name="organizer"/> </param>
    /// <param name="organizer">sets <see cref="_Facts"/></param>
    public CylinderVolumeFact(CylinderVolumeFact fact, Dictionary<string, string> old_to_new, FactOrganizer organizer) : base(fact, organizer)
    {
        init(old_to_new[fact.Cid1], old_to_new[fact.Cid2], fact.vol, old_to_new[fact.equalCirclesProof], fact.proof);
    }

    /// <summary>
    /// Standard Constructor
    /// </summary>
    /// <param name="cid1">sets <see cref="Cid1"/></param>
    /// <param name="cid2">sets <see cref="Cid2"/></param>
    /// <param name="vol">sets <see cref="vol"/></param>
    /// <param name="proof">sets <see cref="proof"/></param>
    /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    public CylinderVolumeFact(string cid1, string cid2, float vol, string eqProof, OMA proof, FactOrganizer organizer) : base(organizer)
    {
        init(cid1, cid2, vol, eqProof, proof);
    }

    /// <summary>
    /// sets variables and generates MMT Declaration
    /// </summary>
    /// <param name="cid1">sets <see cref="Cid1"/></param>
    /// <param name="cid2">sets <see cref="Cid2"/></param>
    /// <param name="vol">sets <see cref="vol"/></param>
    /// <param name="proof">sets <see cref="proof"/></param>
    private void init(string cid1, string cid2, float vol, string eqProof, OMA proof)
    {
        this.Cid1 = cid1;
        this.Cid2 = cid2;
        this.proof = proof;
        this.equalCirclesProof = eqProof;

        CircleFact cf1 = _Facts[cid1] as CircleFact;
        CircleFact cf2 = _Facts[cid2] as CircleFact;
        EqualCirclesFact pf1 = _Facts[eqProof] as EqualCirclesFact;
        this.vol = vol;


        MMTDeclaration mmtDecl;
        string c1URI = cf1.Id;
        string c2URI = cf2.Id;
        string p1Uri = pf1.Id;


        mmtDecl = generateMMTDeclaration(c1URI, c2URI, vol,p1Uri, proof);

        AddFactResponse.sendAdd(mmtDecl, out this._URI);
    }

    /// <summary>
    /// Bypasses initialization of new MMT %Fact by using existend URI, _which is not checked for existence_.
    /// </summary>
    /// <param name="Cid1">sets <see cref="Cid1"/></param>
    /// <param name="Cid2">sets <see cref="Cid2"/></param>
    /// <param name="volume">sets <see cref="vol"/></param>
    /// <param name="proof">sets <see cref="proof"/></param>
    /// <param name="backendURI">MMT URI</param>
    /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    public CylinderVolumeFact(string Cid1, string Cid2, float volume, string eqProof, OMA proof, string backendURI, FactOrganizer organizer) : base(organizer)
    {
        this.Cid1 = Cid1;
        this.Cid2 = Cid2;
        this.vol = volume;
        this.proof = proof;
        this.equalCirclesProof = eqProof;

        this._URI = backendURI;
        _ = this.Label;
    }

    /// \copydoc Fact.parseFact(Scroll.ScrollFact)
    public new static CylinderVolumeFact parseFact(Scroll.ScrollFact fact)
    {
        string uri = fact.@ref.uri;

        string Circle1Uri = ((OMS)((OMA)((OMA)((Scroll.ScrollValueFact)fact).lhs).arguments[0]).arguments[0]).uri;
        string Circle2Uri = ((OMS)((OMA)((OMA)((Scroll.ScrollValueFact)fact).lhs).arguments[0]).arguments[1]).uri;
        float volume = ((OMF)((Scroll.ScrollValueFact)fact).value).f;
        string EqualCirclesProof = ((OMS)(((OMA)((OMA)((Scroll.ScrollValueFact)fact).lhs).arguments[0]).arguments[2])).uri;



        OMA proof = (OMA)(((OMA)((OMA)((Scroll.ScrollValueFact)fact).lhs).arguments[0]).arguments[3]);

        if (StageStatic.stage.factState.ContainsKey(Circle1Uri) && StageStatic.stage.factState.ContainsKey(Circle2Uri))

            return new CylinderVolumeFact(Circle1Uri, Circle2Uri, volume, EqualCirclesProof, proof, uri, StageStatic.stage.factState);

        else    //If dependent facts do not exist return null
            return null;
    }

    /// \copydoc Fact.generateLabel
    protected override string generateLabel()
    {
        return "V(" + _Facts[Cid1].Label + "," + _Facts[Cid2].Label + ")";
    }



    /// <summary>
    /// Constructs struct for not-right-angled MMT %Fact <see cref="AddFactResponse"/>
    /// </summary>
    /// <param name="c1URI"> Uri for <see cref="Cid1"/></param>
    /// <param name="c2URI"> Uri for <see cref="Cid2"/></param>
    /// <param name="val"> <see cref="vol"/></param>
    /// <returns>struct for <see cref="AddFactResponse"/></returns>
    private MMTDeclaration generateMMTDeclaration(string c1URI, string c2URI, float val, string p1URI, OMA proof)
    {
        MMTTerm lhs =
            new OMA(
                new OMS(MMTURIs.CylinderVolume),

                new List<MMTTerm> {
                    new OMS(c1URI),
                    new OMS(c2URI),
                    new OMS(p1URI),
                    proof,
                }
            );

        MMTTerm valueTp = new OMS(MMTURIs.RealLit);
        MMTTerm value = new OMF(val);

        return new MMTValueDeclaration(this.Label, lhs, valueTp, value);
    }

    /// \copydoc Fact.hasDependentFacts
    public override Boolean hasDependentFacts()
    {
        return true;
    }

    /// \copydoc Fact.getDependentFactIds
    public override string[] getDependentFactIds()
    {
        return new string[] { Cid1, Cid2, equalCirclesProof };
    }

    /// \copydoc Fact.instantiateDisplay(GameObject, Transform)
    public override GameObject instantiateDisplay(GameObject prefab, Transform transform)
    {
        var obj = GameObject.Instantiate(prefab, Vector3.zero, Quaternion.identity, transform);
        obj.transform.GetChild(0).gameObject.GetComponent<TextMeshProUGUI>().text = _Facts[this.Cid1].Label + _Facts[this.Cid2].Label;
        obj.GetComponent<FactWrapper>().fact = this;

        return obj;
    }

    /// \copydoc Fact.GetHashCode
    /// uhhh is this a problem?
    public override int GetHashCode()
    {
        return this.Cid1.GetHashCode() ^ this.Cid2.GetHashCode();
    }

    /// \copydoc Fact.Equivalent(Fact, Fact)
    protected override bool EquivalentWrapped(CylinderVolumeFact f1, CylinderVolumeFact f2)
    {
        if (f1.Cid1 == f2.Cid1 && f1.Cid2 == f2.Cid2)
            return true;

        CircleFact c1f1 = (CircleFact)_Facts[f1.Cid1];
        CircleFact c1f2 = (CircleFact)_Facts[f2.Cid1];

        CircleFact c2f1 = (CircleFact)_Facts[f1.Cid2];
        CircleFact c2f2 = (CircleFact)_Facts[f2.Cid2];

        return (c1f1.Equivalent(c1f2) && c2f1.Equivalent(c2f2) && (Mathf.Abs(f1.vol - f2.vol) < 0.001) );

    }
}

/// <summary>
/// A fact that describes, that two circles have the same size and is comprised of two <see cref="CircleFact">CircleFacts</see> 
/// </summary>
public class EqualCirclesFact : FactWrappedCRTP<EqualCirclesFact>
{
    /// \copydoc Fact.s_type
    [JsonProperty]
    protected static new string s_type = "EqualCirclesFact";

    /// @{ <summary>
    /// two circles that are meant to be equal in area
    /// </summary>
    public string Cid1, Cid2;
    /// @}




    /// <summary> \copydoc Fact.Fact </summary>
    public EqualCirclesFact() : base()
    {
        this.Cid1 = null;
        this.Cid2 = null;
    }

    /// <summary>
    /// Copies <paramref name="fact"/> by initiating new MMT %Fact.
    /// </summary>
    /// <param name="fact">Fact to be copied</param>
    /// <param name="old_to_new"><c>Dictionary</c> mapping <paramref name="fact"/>.<see cref="getDependentFactIds"/> in <paramref name="fact"/>.<see cref="Fact._Facts"/> to corresponding <see cref="Fact.Id"/> in <paramref name="organizer"/> </param>
    /// <param name="organizer">sets <see cref="_Facts"/></param>
    public EqualCirclesFact(EqualCirclesFact fact, Dictionary<string, string> old_to_new, FactOrganizer organizer) : base(fact, organizer)
    {
        init(old_to_new[fact.Cid1], old_to_new[fact.Cid2]);
    }

    /// <summary>
    /// Standard Constructor
    /// </summary>
    /// <param name="cid1">sets <see cref="Cid1"/></param>
    /// <param name="cid2">sets <see cref="Cid2"/></param>
    /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    public EqualCirclesFact(string cid1, string cid2, FactOrganizer organizer) : base(organizer)
    {
        init(cid1, cid2);
    }

    /// <summary>
    /// Initiates <see cref="Cid1"/>, <see cref="Cid2"/>, <see cref="Fact._URI"/> and creates MMT %Fact Server-Side
    /// </summary>
    /// <param name="cid1">sets <see cref="Cid1"/></param>
    /// <param name="cid2">sets <see cref="Cid2"/></param>
    private void init(string cid1, string cid2)
    {
        this.Cid1 = cid1;
        this.Cid2 = cid2;

        CircleFact cf1 = _Facts[cid1] as CircleFact;
        CircleFact cf2 = _Facts[cid2] as CircleFact;

        MMTDeclaration mmtDecl;
        string c1URI = cf1.Id;
        string c2URI = cf2.Id;
        mmtDecl = generateEqualCirclesFactDeclaration(c1URI, c2URI);

        AddFactResponse.sendAdd(mmtDecl, out this._URI);
    }

    /// <summary>
    /// Bypasses initialization of new MMT %Fact by using existend URI, _which is not checked for existence_.
    /// </summary>
    /// <param name="Cid1">sets <see cref="Cid1"/></param>
    /// <param name="Cid2">sets <see cref="Cid2"/></param>
    /// <param name="backendURI">MMT URI</param>
    /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    public EqualCirclesFact(string Cid1, string Cid2, string backendURI, FactOrganizer organizer) : base(organizer)
    {
        this.Cid1 = Cid1;
        this.Cid2 = Cid2;

        this._URI = backendURI;
        _ = this.Label;
    }

    /// \copydoc Fact.parseFact(Scroll.ScrollFact)
    public new static EqualCirclesFact parseFact(Scroll.ScrollFact fact)
    {
        OMA tp = (OMA)((Scroll.ScrollSymbolFact)fact).tp;
        if (tp == null)
            return null;

        string circleAUri = "";
        string circleBUri = "";

        string uri = fact.@ref.uri;
        OMA proof_OMA = (OMA)((Scroll.ScrollSymbolFact)fact).tp; // proof DED


        OMA parallel_circles_OMA = (OMA)proof_OMA.arguments[0]; // parallel

        if (parallel_circles_OMA.arguments[0] is OMS)
        {
            // Normaler Fall 
            circleAUri = ((OMS)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[0]).uri;
            circleBUri = ((OMS)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[1]).uri;

        }
        


        if (StageStatic.stage.factState.ContainsKey(circleAUri)
         && StageStatic.stage.factState.ContainsKey(circleBUri))

            return new EqualCirclesFact(circleAUri, circleBUri, uri, StageStatic.stage.factState);

        else    //If dependent facts do not exist return null
            return null;
    }

    /// \copydoc Fact.generateLabel
    protected override string generateLabel()
    {
        return   _Facts[Cid1].Label + " ≠ " + _Facts[Cid2].Label;
    }



    /// <summary>
    /// Constructs struct for equalCirclesFact <see cref="AddFactResponse"/>
    /// </summary>
    /// <param name="c1URI"><see cref="Cid1"/></param>
    /// <param name="c2URI"><see cref="Cid2"/></param>
    /// <returns>struct for <see cref="AddFactResponse"/></returns>
    private MMTDeclaration generateEqualCirclesFactDeclaration(string c1URI, string c2URI)
    {

        List<MMTTerm> innerArguments = new List<MMTTerm>
        {
            new OMS(c1URI),
            new OMS(c2URI)
        };

        List<MMTTerm> outerArguments = new List<MMTTerm>
        {
            new OMA(new OMS(MMTURIs.EqualityCircles), innerArguments)
        };

        //OMS constructor generates full URI
        MMTTerm tp = new OMA(new OMS(MMTURIs.Ded), outerArguments);
        MMTTerm df = null;

        MMTSymbolDeclaration mmtDecl = new MMTSymbolDeclaration(this.Label, tp, df);
        AddFactResponse.sendAdd(mmtDecl, out this._URI);


        return mmtDecl;
    }


    /// \copydoc Fact.hasDependentFacts
    public override Boolean hasDependentFacts()
    {
        return true;
    }

    /// \copydoc Fact.getDependentFactIds
    public override string[] getDependentFactIds()
    {
        return new string[] { Cid1, Cid2 };
    }

    /// \copydoc Fact.instantiateDisplay(GameObject, Transform)
    public override GameObject instantiateDisplay(GameObject prefab, Transform transform)
    {
        var obj = GameObject.Instantiate(prefab, Vector3.zero, Quaternion.identity, transform);
        obj.transform.GetChild(0).gameObject.GetComponent<TextMeshProUGUI>().text = _Facts[this.Cid1].Label;
        obj.transform.GetChild(1).gameObject.GetComponent<TextMeshProUGUI>().text = _Facts[this.Cid2].Label;
        obj.GetComponent<FactWrapper>().fact = this;
        return obj;
    }

    /// \copydoc Fact.GetHashCode
    public override int GetHashCode()
    {
        return this.Cid1.GetHashCode() ^ this.Cid2.GetHashCode();
    }

    /// \copydoc Fact.Equivalent(Fact, Fact)
    protected override bool EquivalentWrapped(EqualCirclesFact f1, EqualCirclesFact f2)
    {
        if ((f1.Cid1 == f2.Cid1 && f1.Cid2 == f2.Cid2))
            return true;

        CircleFact e1f1 = (CircleFact)_Facts[f1.Cid1];
        CircleFact e2f1 = (CircleFact)_Facts[f1.Cid2];
        CircleFact e1f2 = (CircleFact)_Facts[f2.Cid1];
        CircleFact e2f2 = (CircleFact)_Facts[f2.Cid2];

        return (e1f1.Equivalent(e1f2) && e2f1.Equivalent(e2f2));
    }
}

/// <summary>
/// A fact that describes, that two circles have not the same size and is comprised of two <see cref="CircleFact">CircleFacts</see> 
/// </summary>
public class UnEqualCirclesFact : FactWrappedCRTP<UnEqualCirclesFact>
{
    /// \copydoc Fact.s_type
    [JsonProperty]
    protected static new string s_type = "UnEqualCirclesFact";

    /// @{ <summary>
    /// two circles that are meant to be unequal in area
    /// </summary>
    public string Cid1, Cid2;
    /// @}




    /// <summary> \copydoc Fact.Fact </summary>
    public UnEqualCirclesFact() : base()
    {
        this.Cid1 = null;
        this.Cid2 = null;
    }

    /// <summary>
    /// Copies <paramref name="fact"/> by initiating new MMT %Fact.
    /// </summary>
    /// <param name="fact">Fact to be copied</param>
    /// <param name="old_to_new"><c>Dictionary</c> mapping <paramref name="fact"/>.<see cref="getDependentFactIds"/> in <paramref name="fact"/>.<see cref="Fact._Facts"/> to corresponding <see cref="Fact.Id"/> in <paramref name="organizer"/> </param>
    /// <param name="organizer">sets <see cref="_Facts"/></param>
    public UnEqualCirclesFact(UnEqualCirclesFact fact, Dictionary<string, string> old_to_new, FactOrganizer organizer) : base(fact, organizer)
    {
        init(old_to_new[fact.Cid1], old_to_new[fact.Cid2]);
    }

    /// <summary>
    /// Standard Constructor
    /// </summary>
    /// <param name="cid1">sets <see cref="Cid1"/></param>
    /// <param name="cid2">sets <see cref="Cid2"/></param>
    /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    public UnEqualCirclesFact(string cid1, string cid2, FactOrganizer organizer) : base(organizer)
    {
        init(cid1, cid2);
    }

    /// <summary>
    /// Initiates <see cref="Cid1"/>, <see cref="Cid2"/>, <see cref="Fact._URI"/> and creates MMT %Fact Server-Side
    /// </summary>
    /// <param name="cid1">sets <see cref="Cid1"/></param>
    /// <param name="cid2">sets <see cref="Cid2"/></param>
    private void init(string cid1, string cid2)
    {
        
        this.Cid1 = cid1;
        this.Cid2 = cid2;

        CircleFact cf1 = _Facts[cid1] as CircleFact;
        CircleFact cf2 = _Facts[cid2] as CircleFact;

        MMTDeclaration mmtDecl;
        string c1URI = cf1.Id;
        string c2URI = cf2.Id;
        mmtDecl = generateUnEqualCirclesFactDeclaration(c1URI, c2URI);

        AddFactResponse.sendAdd(mmtDecl, out this._URI);
    }

    /// <summary>
    /// Bypasses initialization of new MMT %Fact by using existend URI, _which is not checked for existence_.
    /// </summary>
    /// <param name="Cid1">sets <see cref="Cid1"/></param>
    /// <param name="Cid2">sets <see cref="Cid2"/></param>
    /// <param name="backendURI">MMT URI</param>
    /// <param name="organizer">sets <see cref="Fact._Facts"/></param>
    public UnEqualCirclesFact(string Cid1, string Cid2, string backendURI, FactOrganizer organizer) : base(organizer)
    {
        this.Cid1 = Cid1;
        this.Cid2 = Cid2;

        this._URI = backendURI;
        _ = this.Label;
    }

    /// \copydoc Fact.parseFact(Scroll.ScrollFact)
    public new static UnEqualCirclesFact parseFact(Scroll.ScrollFact fact)
    {
        OMA tp = (OMA)((Scroll.ScrollSymbolFact)fact).tp;
        if (tp == null)
            return null;

        string circleAUri = "";
        string circleBUri = "";

        string uri = fact.@ref.uri;
        OMA proof_OMA = (OMA)((Scroll.ScrollSymbolFact)fact).tp; // proof DED


        OMA unequal_circles_OMA = (OMA)proof_OMA.arguments[0]; // unequal

        if (unequal_circles_OMA.arguments[0] is OMS)
        {
            // Normaler Fall 
            circleAUri = ((OMS)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[0]).uri;
            circleBUri = ((OMS)((OMA)((OMA)((Scroll.ScrollSymbolFact)fact).tp).arguments[0]).arguments[1]).uri;

        }



        if (StageStatic.stage.factState.ContainsKey(circleAUri)
         && StageStatic.stage.factState.ContainsKey(circleBUri))

            return new UnEqualCirclesFact(circleAUri, circleBUri, uri, StageStatic.stage.factState);

        else    //If dependent facts do not exist return null
            return null;
    }

    /// \copydoc Fact.generateLabel
    protected override string generateLabel()
    {
        return _Facts[Cid1].Label + " = " + _Facts[Cid2].Label;
    }



    /// <summary>
    /// Constructs struct for equalCirclesFact <see cref="AddFactResponse"/>
    /// </summary>
    /// <param name="c1URI"><see cref="Cid1"/></param>
    /// <param name="c2URI"><see cref="Cid2"/></param>
    /// <returns>struct for <see cref="AddFactResponse"/></returns>
    private MMTDeclaration generateUnEqualCirclesFactDeclaration(string c1URI, string c2URI)
    {

        List<MMTTerm> innerArguments = new List<MMTTerm>
        {
            new OMS(c1URI),
            new OMS(c2URI)
        };

        List<MMTTerm> outerArguments = new List<MMTTerm>
        {
            new OMA(new OMS(MMTURIs.UnEqualityCircles), innerArguments)
        };

        //OMS constructor generates full URI
        MMTTerm tp = new OMA(new OMS(MMTURIs.Ded), outerArguments);
        MMTTerm df = null;

        MMTSymbolDeclaration mmtDecl = new MMTSymbolDeclaration(this.Label, tp, df);
        AddFactResponse.sendAdd(mmtDecl, out this._URI);


        return mmtDecl;
    }


    /// \copydoc Fact.hasDependentFacts
    public override Boolean hasDependentFacts()
    {
        return true;
    }

    /// \copydoc Fact.getDependentFactIds
    public override string[] getDependentFactIds()
    {
        return new string[] { Cid1, Cid2 };
    }

    /// \copydoc Fact.instantiateDisplay(GameObject, Transform)
    public override GameObject instantiateDisplay(GameObject prefab, Transform transform)
    {
        var obj = GameObject.Instantiate(prefab, Vector3.zero, Quaternion.identity, transform);
        obj.transform.GetChild(0).gameObject.GetComponent<TextMeshProUGUI>().text = _Facts[this.Cid1].Label;
        obj.transform.GetChild(1).gameObject.GetComponent<TextMeshProUGUI>().text = _Facts[this.Cid2].Label;
        obj.GetComponent<FactWrapper>().fact = this;
        return obj;
    }

    /// \copydoc Fact.GetHashCode
    public override int GetHashCode()