Theory AxSelfMinus

(*
   Mike Stannett
   Feb 2023
*)

section ‹ AXIOM: AxSelfMinus ›

text ‹This theory declares the axiom AxSelfMinus.›

theory AxSelfMinus
  imports WorldView
begin

text ‹AxSelfMinus:
  The worldline of an observer is a subset of the time axis in their own
  worldview.›

(*
  (∀m ∈ Ob) wline_m(m) ⊆ t-axis
*)
class axSelfMinus = WorldView
begin
  abbreviation axSelfMinus :: "Body ⇒ 'a Point ⇒ bool" 
    where "axSelfMinus m p ≡ (m sees m at p) ⟶ onTimeAxis p"
end (* of class axSelfMinus *)


class AxSelfMinus = axSelfMinus +
  assumes AxSelfMinus : "∀ m p    . axSelfMinus  m p"
begin
end (* of class AxSelfMinus *)

end (* of theory AxSelfMinus *)