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


tff(x_decl, type, x: $o).


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

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

tff(model_mapping, interpretation-mappings,
($in_world(world_0,
	(~x))
& $in_world(world_1,
	(~x))
)).