(* *)
(**************************************************************************)
-include "ground_2/notation/relations/ringeq_3.ma".
+include "ground/notation/relations/ringeq_3.ma".
include "apps_2/notation/models/at_3.ma".
+include "apps_2/notation/models/oplus_4.ma".
include "apps_2/notation/models/wbrackets_4.ma".
include "static_2/syntax/term.ma".
sq: relation2 dd dd;
(* Note: sort evaluation *)
sv: nat → dd;
+(* Note: conjunction *)
+ co: bool → dd → dd → dd;
(* Note: application *)
ap: dd → dd → dd;
(* Note: term interperpretation *)
interpretation "application (model)"
'At M d1 d2 = (ap M d1 d2).
+interpretation "conjunction (model)"
+ 'OPlus M p d1 d2 = (co M p d1 d2).
+
interpretation "term interpretation (model)"
'WBrackets M gv lv T = (ti M gv lv T).