Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: allen_interval_properties.pvs Sprache: PVS

Original von: PVS^©

allen_interval_properties : THEORY
BEGIN
  IMPORTING allen_interval

% The Transitivity Temporal lemmas

  A, B, C: VAR StrictInterval

  before_before: LEMMA <(A, B) AND <(B, C) IMPLIES <(A, C)

  before_during: LEMMA A < B AND d(B, C) IMPLIES
                      A < C OR o(A, C) OR m(A, C) OR d(A, C) OR s(A, C)

  before_contains: LEMMA <(A, B) AND di(B, C) IMPLIES <(A, C)

  before_overlaps: LEMMA <(A, B) AND o(B, C) IMPLIES <(A, C)

  before_overlapped_by: LEMMA <(A, B) AND oi(B, C) IMPLIES
                              <(A, C) OR o(A, C) OR m(A, C) OR d(A, C) OR s(A, C)

  before_meets: LEMMA <(A, B) AND m(B, C) IMPLIES <(A, C)

  before_met_by: LEMMA <(A, B) AND mi(B, C) IMPLIES
                       <(A, C) OR o(A, C) OR m(A, C) OR d(A, C) OR s(A, C)

  before_starts :LEMMA <(A, B) AND s(B, C) IMPLIES <(A, C)

  before_started_by :LEMMA <(A, B) AND si(B, C) IMPLIES <(A, C)

  before_finishes :LEMMA <(A, B) AND f(B, C) IMPLIES
                            <(A, C) OR o(A, C) OR m(A, C) OR d(A, C) OR s(A, C)

  before_finished_by :LEMMA <(A, B) AND fi(B, C) IMPLIES <(A, C)

  after_after:LEMMA >(A, B) AND >(B, C) IMPLIES >(A, C)

  after_during :LEMMA >(A, B) AND d(B, C) IMPLIES
                   >(A, C) OR oi(A, C) OR mi(A, C) OR d(A, C) OR f(A, C)

  after_contains :LEMMA >(A, B) AND di(B, C) IMPLIES >(A, C)

  after_overlaps :LEMMA >(A, B) AND o(B, C) IMPLIES
                   >(A, C) OR oi(A, C) OR mi(A, C) OR d(A, C) OR f(A, C)

  after_meets :LEMMA >(A, B) AND m(B, C) IMPLIES
                   >(A, C) OR oi(A, C) OR mi(A, C) OR d(A, C) OR f(A, C)

  after_met_by :LEMMA >(A, B) AND mi(B, C) IMPLIES >(A, C)

  after_starts :LEMMA >(A, B) AND s(B, C) IMPLIES
                   >(A, C) OR oi(A, C) OR mi(A, C) OR d(A, C) OR f(A, C)

  after_started_by :LEMMA >(A, B) AND si(B, C) IMPLIES >(A, C)

  after_finishes :LEMMA >(A, B) AND f(B, C) IMPLIES >(A, C)

  after_finished_by :LEMMA >(A, B) AND fi(B, C) IMPLIES >(A, C)

  during_before :LEMMA d(A, B) AND >(B, C) IMPLIES >(A, C)

  during_after :LEMMA d(A, B) AND <(B, C) IMPLIES <(A, C)

  during_during :LEMMA d(A, B) AND d(B, C) IMPLIES d(A, C)

  during_overlaps :LEMMA d(A, B) AND o(B, C) IMPLIES
                       <(A, C) OR o(A, C) OR m(A, C) OR d(A, C) OR s(A, C)

  during_overlapped_by:LEMMA d(A, B) AND oi(B, C) IMPLIES
                            >(A, C) OR oi(A, C) OR mi(A, C) OR d(A, C) OR f(A, C)

  during_meets :LEMMA d(A, B) AND m(B, C) IMPLIES <(A, C)

  during_t_meet_bay :LEMMA d(A, B) AND mi(B, C) IMPLIES >(A, C)

  during_starts :LEMMA d(A, B) AND s(B, C) IMPLIES d(A, C)

  during_started_by :LEMMA d(A, B) AND si(B, C) IMPLIES
                            >(A, C) OR oi(A, C) OR mi(A, C) OR d(A, C) OR f(A, C)

  during_finished_by: LEMMA d(A, B) AND fi(B, C) IMPLIES
                         <(A, C) OR o(A, C) OR m(A, C) OR d(A, C) OR s(A, C)

  during_finishes:LEMMA d(A, B) AND f(B, C) IMPLIES  d(A, C)

  contains_before:LEMMA di(A, B) AND <(B, C) IMPLIES
                      <(A, C) OR o(A, C) OR m(A, C) OR di(A, C) OR fi(A, C)

  contains_after :LEMMA di(A, B) AND >(B, C) IMPLIES
                        >(A, C) OR oi(A, C) OR mi(A, C) OR di(A, C) OR si(A, C)

  contains_during: LEMMA di(A, B) AND d(B, C) IMPLIES
                         o(A, C) OR oi(A, C) OR dur(A, C) OR con(A, C) OR A = C

  contains_contains :LEMMA di(A, B) AND di(B, C) IMPLIES di(A, C)

  contains_overlaps :LEMMA di(A, B) AND o(B, C) IMPLIES
                        o(A, C) OR di(A, C) OR fi(A, C)

  contains_overlapped_by :LEMMA di(A, B) AND oi(B, C) IMPLIES
                             oi(A, C) OR di(A, C) OR si(A, C)

  contains_meets :LEMMA di(A, B) AND m(B, C) IMPLIES
                      o(A, C) OR di(A, C) OR fi(A, C)

  contains_meet_by :LEMMA di(A, B) AND mi(B, C) IMPLIES
                      oi(A, C) OR di(A, C) OR si(A, C)

  contains_starts :LEMMA di(A, B) AND s(B, C) IMPLIES
                      di(A, C) OR fi(A, C) OR o(A, C)

  contains_started_by:LEMMA di(A, B) AND si(B, C) IMPLIES di(A, C)

  contains_finishes :LEMMA di(A, B) AND f(B, C) IMPLIES
                        di(A, C) OR si(A, C) OR oi(A, C)

  contains_finished_by :LEMMA di(A, B) AND fi(B, C) IMPLIES di(A, C)

  overlaps_before:LEMMA o(A, B) AND <(B, C) IMPLIES <(A, C)

  overlaps_after :LEMMA o(A, B) AND >(B, C) IMPLIES
                     >(A, C) OR oi(A, C) OR mi(A, C) OR di(A, C) OR si(A, C)

  overlaps_during:LEMMA o(A, B) AND d(B, C) IMPLIES  o(A, C) OR d(A, C) OR s(A, C)

  overlaps_overlapped_by: LEMMA o(A, B) AND oi(B,C) IMPLIES
                              o(A,C) OR  oi(A,C) OR dur(A,C) OR con(A,C) OR A = C

  overlaps_contains :LEMMA o(A, B) AND di(B, C) IMPLIES
                        <(A, C) OR o(A, C) OR m(A, C) OR di(A, C) OR fi(A, C)

  overlaps_overlaps: LEMMA o(A, B) AND o(B, C) IMPLIES
                        <(A, C) OR o(A, C) OR m(A, C)

  overlaps_meets: LEMMA o(A, B) AND m(B, C) IMPLIES  <(A, C)

  overlaps_met_by: LEMMA o(A, B) AND mi(B, C) IMPLIES oi(A, C) OR di(A, C) OR si(A, C)

  overlaps_starts: LEMMA o(A, B) AND s(B, C) IMPLIES o(A, C)

  overlaps_start_by: LEMMA o(A, B) AND si(B, C) IMPLIES di(A, C) OR o(A, C) OR fi(A, C)

  overlaps_finishes: LEMMA o(A, B) AND f(B, C) IMPLIES  d(A, C) OR o(A, C) OR s(A, C)

  overlaps_finished_by:LEMMA o(A, B) AND fi(B, C) IMPLIES
                        <(A, C) OR o(A, C) OR m(A, C)

  overlapped_by_before: LEMMA oi(A, B) AND <(B, C) IMPLIES
                           <(A, C) OR o(A, C) OR m(A, C) OR di(A, C) OR fi(A, C)

  overlapped_by_after: LEMMA oi(A, B) AND >(B, C) IMPLIES  >(A, C)

  overlapped_by_during: LEMMA oi(A, B) AND d(B, C) IMPLIES
                           oi(A, C) OR d(A, C) OR f(A, C)

  overlapped_by_contains: LEMMA oi(A, B) AND di(B, C) IMPLIES
                             >(A, C) OR oi(A, C) OR di(A, C) OR mi(A, C) OR si(A, C)

  overlapped_by_overlaps: LEMMA o(A, B) AND oi(B,C) IMPLIES
                              o(A,C) OR  oi(A,C) OR dur(A,C) OR con(A,C) OR A = C

  overlapped_by_overlapped_by: LEMMA oi(A, B) AND oi(B, C) IMPLIES
                                  >(A, C) OR oi(A, C) OR mi(A, C)

  overlapped_by_meets: LEMMA oi(A, B) AND m(B, C) IMPLIES
                                  o(A, C) OR fi(A, C) OR di(A, C)

  overlapped_by_meet_by: LEMMA oi(A, B) AND mi(B, C) IMPLIES >(A, C)

  overlapped_by_starts: LEMMA oi(A, B) AND s(B, C) IMPLIES
                           oi(A, C) OR d(A, C) OR f(A, C)

  overlapped_by_started_by: LEMMA oi(A, B) AND si(B, C) IMPLIES
                               >(A, C) OR oi(A, C) OR mi(A, C)

  overlapped_by_finishes: LEMMA oi(A, B) AND f(B, C) IMPLIES oi(A, C)

  overlapped_by_finished_by: LEMMA oi(A, B) AND fi(B, C) IMPLIES
                                oi(A, C) OR di(A, C) OR si(A, C)

  meets_before: LEMMA m(A, B) AND <(B, C) IMPLIES <(A, C)

  meets_after: LEMMA m(A, B) AND >(B, C) IMPLIES
                  >(A, C) OR oi(A, C) OR mi(A, C) OR di(A, C) OR si(A, C)

  meets_during: LEMMA m(A, B) AND d(B, C) IMPLIES
                   o(A, C) OR d(A, C) OR s(A, C)

  meets_contains: LEMMA m(A, B) AND di(B, C) IMPLIES <(A, C)

  meets_overlaps: LEMMA m(A, B) AND o(B, C) IMPLIES <(A, C)

  meets_overlapped_by: LEMMA m(A, B) AND oi(B, C) IMPLIES
                          o(A, C) OR d(A, C) OR s(A, C)

  meets_meets: LEMMA m(A, B) AND m(B, C) IMPLIES A < C

  meets_meet_by: LEMMA m(A, B) AND mi(B, C) IMPLIES
                    f(A, C) OR fi(A, C) OR A = C

  meets_starts: LEMMA m(A, B) AND s(B, C) IMPLIES m(A, C)

  meets_started_by: LEMMA m(A, B) AND si(B, C) IMPLIES m(A, C)

  meets_finishes: LEMMA m(A, B) AND f(B, C) IMPLIES
                     d(A, C) OR s(A, C) OR o(A, C)

  meets_finished_by: LEMMA m(A, B) AND fi(B, C) IMPLIES <(A, C)

  meet_by_before: LEMMA mi(A, B) AND <(B, C) IMPLIES
                     <(A, C) OR o(A, C) OR m(A, C) OR di(A, C)OR fi(A, C)

  meet_by_after: LEMMA mi(A, B) AND >(B, C) IMPLIES >(A, C)

  meet_by_during: LEMMA mi(A, B) AND d(B, C) IMPLIES
                     oi(A, C)OR d(A, C) OR f(A, C)

  meet_by_contains: LEMMA mi(A, B) AND di(B, C) IMPLIES >(A, C)

  meet_by_overlaps: LEMMA mi(A, B) AND o(B, C) IMPLIES
                       oi(A, C)OR d(A, C)OR f(A, C)

  meet_by_meet: LEMMA mi(A, B) AND m(B, C) IMPLIES
                            si(A, C)OR s(A, C)OR A = C

  meet_by_overlapped_by: LEMMA mi(A, B) AND oi(B, C) IMPLIES >(A, C)

  meet_by_meet_by: LEMMA mi(A, B) AND mi(B, C) IMPLIES >(A, C)

  meet_by_starts: LEMMA mi(A, B) AND s(B, C) IMPLIES
                     d(A, C) OR f(A, C) OR oi(A, C)

  meet_by_started_by: LEMMA mi(A, B) AND si(B, C) IMPLIES A > C

  meet_by_finishes: LEMMA mi(A, B) AND f(B, C) IMPLIES mi(A, C)

  met_by_finished: LEMMA mi(A, B) AND fi(B, C) IMPLIES mi(A, C)

  starts_by_before: LEMMA s(A, B) AND <(B, C) IMPLIES <(A, C)

  starts_by_after: LEMMA s(A, B) AND >(B, C) IMPLIES >(A, C)

  starts_by_during: LEMMA s(A, B) AND d(B, C) IMPLIES d(A, C)

  starts_by_contains: LEMMA s(A, B) AND di(B, C) IMPLIES
                         <(A, C) OR o(A, C) OR m(A, C) OR di(A, C)
                         OR fi(A, C)

  starts_by_overlaps: LEMMA s(A, B) AND o(B, C) IMPLIES
                         <(A, C) OR o(A, C) OR m(A, C)

  starts_by_overlapped_by: LEMMA s(A, B) AND oi(B, C) IMPLIES
                              oi(A, C) OR d(A, C) OR f(A, C)

  starts_by_meet: LEMMA s(A, B) AND m(B, C) IMPLIES A < C

  starts_by_meet_by: LEMMA s(A, B) AND mi(B, C) IMPLIES mi(B, C)

  starts_by_starts: LEMMA s(A, B) AND s(B, C) IMPLIES s(B, C)

  starts_by_started_by: LEMMA s(A, B) AND si(B, C) IMPLIES
                           s(B, C) OR si(B, C) OR A = C

  starts_by_finishes: LEMMA s(A, B) AND f(B, C) IMPLIES d(A, C)

  starts_by_finished_by :LEMMA s(A, B) AND fi(B, C) IMPLIES
                            o(A, C) OR m(A, C) OR <(A, C)

  started_by_before: LEMMA si(A, B) AND <(B, C) IMPLIES
                        o(A, C) OR m(A, C) OR <(A, C) OR di(A, C) OR fi(A, C)

  started_by_after: LEMMA si(A, B) AND >(B, C) IMPLIES >(A, C)

  started_by_during: LEMMA si(A, B) AND d(B, C) IMPLIES
                        oi(A, C) OR d(A, C) OR f(A, C)

  started_by_contains: LEMMA si(A, B) AND di(B, C) IMPLIES di(A, C)

  started_by_overlaps: LEMMA si(A, B) AND o(B, C) IMPLIES
                          di(A, C) OR fi(A, C) OR o(A, C)

  started_by_overlapped_by: LEMMA si(A, B) AND oi(B, C) IMPLIES oi(A, C)

  started_by_meet: LEMMA si(A, B) AND m(B, C) IMPLIES
                      di(A, C) OR fi(A, C) OR o(A, C)

  started_by_meet_by: LEMMA si(A, B) AND mi(B, C) IMPLIES mi(A, C)

  started_by_starts: LEMMA si(A, B) AND s(B, C) IMPLIES
                          si(A, C) OR s(A, C) OR A = C

  started_by_started_by: LEMMA si(A, B) AND si(B, C) IMPLIES si(A, C)

  started_by_finishes: LEMMA si(A, B) AND f(B, C) IMPLIES oi(A, C)

  started_by_finished_by: LEMMA si(A, B) AND fi(B, C) IMPLIES di(A, C)

  finishes_before: LEMMA f(A, B) AND <(B, C) IMPLIES <(A, C)

  finishes_after: LEMMA f(A, B) AND >(B, C) IMPLIES >(A, C)

  finishes_during :LEMMA f(A, B) AND d(B, C) IMPLIES d(A, C)

  finishes_contains: LEMMA f(A, B) AND di(B, C) IMPLIES
                        >(A, C) OR oi(A, C) OR mi(A, C) OR di(A, C) OR si(A, C)

  finishes_overlaps:  LEMMA f(A, B) AND o(B, C) IMPLIES
                        o(A, C) OR d(A, C) OR s(A, C)

  finishes_overlapped_by: LEMMA f(A, B) AND oi(B, C) IMPLIES
                              >(A, C) OR mi(A, C) OR oi(A, C)

  finishes_meets: LEMMA f(A, B) AND m(B, C) IMPLIES m(A, C)

  finishes_meet_by: LEMMA f(A, B) AND mi(B, C) IMPLIES >(A, C)

  finishes_starts: LEMMA f(A, B) AND s(B, C) IMPLIES d(A, C)

  finishes_started_by: LEMMA f(A, B) AND si(B, C) IMPLIES
                          >(A, C) OR mi(A, C) OR oi(A, C)

  finishes_finishes: LEMMA f(A, B) AND f(B, C) IMPLIES f(A, C)

  finishes_finished_by: LEMMA f(A, B) AND fi(B, C) IMPLIES
                           f(A, C) OR fi(A, C) OR A = C

  finished_by_before: LEMMA fi(A, B) AND <(B, C) IMPLIES A < C

  finished_by_after: LEMMA fi(A, B) AND >(B, C) IMPLIES
                         >(A, C) OR mi(A, C) OR oi(A, C) OR di(A, C) OR si(A, C)

  finished_by_during: LEMMA fi(A, B) AND d(B, C) IMPLIES
                         o(A, C) OR d(A, C) OR s(A, C)

  finished_by_contains: LEMMA fi(A, B) AND di(B, C) IMPLIES di(A, C)

  finished_by_overlaps: LEMMA fi(A, B) AND o(B, C) IMPLIES o(A, C)

  finished_by_overlapped_by: LEMMA fi(A, B) AND oi(B, C) IMPLIES
                                oi(A, C) OR di(A, C) OR si(A, C)

  finished_by_meets: LEMMA fi(A, B) AND m(B, C) IMPLIES m(A, C)

  finished_by_meet_by: LEMMA fi(A, B) AND mi(B, C) IMPLIES
                          oi(A, C) OR di(A, C) OR si(A, C)

  finished_by_starts: LEMMA fi(A, B) AND s(B, C) IMPLIES o(A, C)

  finished_by_started_by :LEMMA fi(A, B) AND si(B, C) IMPLIES di(A, C)

  finished_by_finishes:LEMMA fi(A, B) AND f(B, C) IMPLIES
                           f(A, C) OR fi(A, C) OR A = C

  finished_by_finished_by: LEMMA fi(A, B) AND fi(B, C) IMPLIES fi(B, C)

END allen_interval_properties

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.