(note TQC2b2)
(minLang thf)

;thf(mod_tp,type,(mod : $tType)).
;thf(world_tp,type,(world : $tType)).
;thf(accreln_tp,type,(accreln : (world > world > $o))).
;thf(lObligation_type, type, lObligation: mod).
;thf(lPermission_type, type, lPermission: mod).
;thf(lProhibition_type, type, lProhibition: $i).
;thf(lForm_type, type, lForm: (world > $o)).

;thf(modalAttribute_THFTYPE_IoioI_type, type, modalAttribute: ((world > $o) > mod > (world > $o))).

;thf(m1,axiom,(! [A:(world > $o)] : (! [W:world] : ((modalAttribute @ A @ lPermission @ W) <=> (? [U:world] : ((accreln @ W @ U) & (A @ U))))))).
;thf(m2,axiom,(! [A:(world > $o)] : (! [W:world] : ((modalAttribute @ A @ lObligation @ W) <=> (! [U:world] : ((accreln @ W @ U) => (A @ U))))))).

;thf(t22,axiom,((! [A:(world > $o)]: (! [W:world] : ((modalAttribute @ A @ lPermission @ W) =>
;  (~ (modalAttribute @ (^ [U:world] : (~ (A @ U))) @ lObligation @ W))))))).

;thf(t23,axiom,((! [A:(world > $o)]: (! [W:world] : ((modalAttribute @ A @ lObligation @ W) =>
;  (modalAttribute @ A @ lPermission @ W)))))).

;thf(w_tp,type,(w : world)).

;thf(t2,axiom,(((modalAttribute @ lForm @ lObligation @ w)))).

;thf(t1,conjecture,((? [B:(world > $o)]: (modalAttribute @ B @ lPermission @ w)))).

(=>
  (modalAttribute ?A Permission)
  (not
    (modalAttribute
      (not ?A)
      Obligation)))

(=>
  (modalAttribute ?A Obligation)
  (modalAttribute ?A Permission))

(modalAttribute Form Obligation)

(query (modalAttribute ?B Permission))

(answer yes)