tff(simple_K, logic, ($modal) == ([($domains) == ($varying),($designation) == ($rigid),($terms) == ($global),($modalities) == ($modal_system_K)])).


tff(p_type, type, p: (($i) > $o)).


tff(indiv_0_decl, type, indiv_0: $i).

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,
($in_world(world_0, 
	((! [DO: $i]: ( (DO = indiv_0) ))
	&(? [DO: $i]: (DO = indiv_0))))
)).


tff(model_mapping, interpretation-mappings,
($in_world(world_0,
	((! [V1: $i]: p(V1))))
)).