tff(modal_system, logic, ($modal) == ([($domains) == ($constant),($designation) == ($rigid),($terms) == ($local),($modalities) == ($modal_system_K)])).

tff(new_type, type, new: $tType).

tff(newc_decl, type, newc: new).
tff(newf_decl, type, newf: ((new * $i) > new)).
tff(newp_decl, type, newp: ((new * $i) > $o)).
tff(a_decl, type, a: $i).


tff(indiv_0_decl, type, indiv_0: $i).
tff(d_new_decl, type, d_new: $tType).
tff(d2new_decl, type, d2new: d_new > new).
tff(d_new_0_decl, type, d_new_0: d_new).

tff(world_0_decl, type, world_0: $world).

tff(model_worlds, interpretation-worlds, 
((! [W: $world] : ( (W = world_0) ))
& ($local_world = world_0)
& (! [W: $world, V: $world]: $accessible_world(W, V))
)).

tff(model_domains, interpretation-domains,
((! [W: $world]: ($in_world(W,
	((! [DO: $i]: ( (DO = indiv_0) ))
	&(? [DO: $i ]: (DO = indiv_0))))))

& (! [W: $world]: ($in_world(W,
	((! [O: new]: (? [DO: d_new]: O = d2new(DO)))
	& (! [DO1: d_new, DO2: d_new]: ( (d2new(DO1) = d2new(DO2)) => (DO1 = DO2) ))
	& (! [DO: d_new]: ( (DO = d_new_0) ))
	& (? [DO: d_new]: (DO = d_new_0))))))
)).


tff(model_mapping, interpretation-mappings,
($in_world(world_0,
	((newc = d2new(d_new_0))
	& (! [V0: new, V1: $i]: (newf(V0, V1) =  d2new(d_new_0)))
	& (! [V1: new, V2: $i]: newp(V1, V2))
	& (a = indiv_0)))
)).