tff(k_u_f_l, logic, ($modal) == ([($domains) == ($cumulative),($designation) == ($flexible),($terms) == ($local),($modalities) == ($modal_system_K)])).


tff(f_decl, type, f: (($i) > $o)).


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

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)
& (! [W: $world, V: $world]: ((~((W = world_1) & (V = world_0)) & ~((W = world_0) & (V = world_0))) => $accessible_world(W,V)))
& (! [W: $world, V: $world]: ((((W = world_1) & (V = world_0)) | ((W = world_0) & (V = world_0))) => ~$accessible_world(W,V))))).

tff(model_domains, interpretation-domains,
($distinct(indiv_0, indiv_1)
& $in_world(world_0, 
	((! [DO: $i]: ( (DO = indiv_1) ))
	&(? [DO: $i]: (DO = indiv_1))))
& $in_world(world_1, 
	((! [DO: $i]: ( (DO = indiv_0) | (DO = indiv_1) ))
	&(? [DO: $i]: (DO = indiv_0))
	& (? [DO: $i ]: (DO = indiv_1))))
)).


tff(model_mapping, interpretation-mappings,
($in_world(world_0,
	((! [V1: $i]: ~(f(V1)))))
& $in_world(world_1,
	(f(indiv_1)
	& (! [V1: $i]: (~((V1 = indiv_1)) => ~f(V1)))))
)).