Extension Name: subst_res.def
Primitive Lexicon: none
Theories Required by this Extension: res_set.th, requires.th, psl_core.th, act_occ.th, subactivity.th,interval.th, complex_act.th, sitcalc.th
Defined Lexicon:
(forall (?a ?r) (iff (superpose_select ?a ?r) (forall (?a1 ?occ1) (if (and (occurrence_of ?occ1 ?a) (subactivity ?a1 ?a) (primitive ?a1)) (exists (?a2 ?r1 ?occ2) (and (subactivity ?a1 ?a2) (subactivity ?a2 ?a) (occurrence_of ?occ2 ?a2) (holds (resource_subset ?r1 ?r) (root_occ ?occ2)) (nondet_select ?a2 ?r1)))))))A resource set is homogeneous iff it is required by a superpose_select activity.
(forall (?a ?r) (iff (homogeneous_set ?r ?a) (exists (?a2) (and (superpose_select ?a2 ?r) (subactivity ?a ?a2)))))
(forall (?a1 ?a2 ?occ) (iff (occurs_over (set_contention ?r) ?occ) (if (and (subactivity ?a1 (set_contention ?r)) (subactivity ?a2 (set_contention ?r))) (and (requires_set ?a1 ?r) (requires_set ?a2 ?r) (concurrent_superpose (set_contention ?r)))))) (forall (?r ?s) (if (poss (set_contention ?r) ?s) (and (forall (?a) (if (subactivity ?a (set_contention ?a)) (homogeneous_set ?r ?a))) (holds (available ?r (set_contention ?r)) ?s))))