new

source/supremecourt.mmt

+namespace http://mathhub.info/MitM/smglom/arithmetics ❚
+
+import base http://mathhub.info/MitM/Foundation ❚
+
+theory person : base:?Logic = 
+  object : type ❙
+  person : object ⟶ bool ❙
+  rights : object ⟶ bool ❙
+  fetus : object ⟶ bool ❙
+  black : object ⟶ bool ❙ 
+❚
+
+theory legal : base:?Logic = 
+  include ?person ❙
+  courtDecision : prop ⟶ type ❙
+  axiom_personRights : ⊦ ∀[x] rights x ⇒ person x ❙
+❚  
+
+theory RoeWade : base:?Logic = 
+  include ?legal ❙
+  include ?person ❙
+  RoeWade1973 : courtDecision (∀[x] fetus x ⇒ ¬ person x) ❙
+❚
+
+theory DredScott : base:?Logic = 
+  include ?legal ❙
+  include ?person ❙
+  DredScott1857 : courtDecision (∀[x] black x ⇒ ¬ person x) ❙
+❚
+
+view RW73DS57 : ?RoeWade -> ?DredScott =
+  fetus = black ❙
+  RoeWade1973 = DredScott1857 ❙
+❚