[ysp-1] follows from [kfj-1] and [ixo-1]

[michaelrabenberg]

Here are three axioms:

(cl:comment "If a has-continuant-part b then if a is an instance of fiat-surface then b is an instance of continuant-fiat-boundary [ysp-1]" (forall (p q t) (if (and (has-continuant-part p q t) (instance-of p fiat-surface t)) (instance-of q continuant-fiat-boundary t))))

(cl:comment "fiat-surface is subclass of continuant-fiat-boundary [kfj-1]" (forall (t x) (if (instance-of x fiat-surface t) (instance-of x continuant-fiat-boundary t))))

(cl:comment "If a has-continuant-part b then if a is an instance of continuant-fiat-boundary then b is an instance of continuant-fiat-boundary [ixo-1]" (forall (p q t) (if (and (has-continuant-part p q t) (instance-of p continuant-fiat-boundary t)) (instance-of q continuant-fiat-boundary t))))

[ysp-1] follows from [kfj-1] and [ixo-1], so perhaps [ysp-1] could be discarded in the interest of streamlining the axioms.

[alanruttenberg]

Agreed.

[alanruttenberg]

I'm going to close this in favor of #111