tff('k_poly_n.0001', logic, ($modal) == ([($modalities) == ($modal_system_K)])).


tff(false_decl, type, false: $o).
tff(p1_decl, type, p1: $o).
tff(p10_decl, type, p10: $o).
tff(p2_decl, type, p2: $o).
tff(p3_decl, type, p3: $o).
tff(p4_decl, type, p4: $o).
tff(p5_decl, type, p5: $o).
tff(p6_decl, type, p6: $o).
tff(p8_decl, type, p8: $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)
& (! [W: $world, V: $world]: $accessible_world(W, V))
)).

tff(model_mapping, interpretation-mappings,
($in_world(world_0,
	(~false
	& ~p10
	& p2
	& p4
	& ~p5
	& ~p6
	& ~p8))
& $in_world(world_1,
	(~false
	& p1
	& ~p10
	& p3
	& ~p5
	& ~p6
	& ~p8))
)).