SSL allen_interval_properties.pvs   Sprache: unbekannt

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