tff('s4_s5_n.0005', logic, ($modal) == ([($modalities) == ($modal_system_S4)])).


tff(false_decl, type, false: $o).
tff(p1_decl, type, p1: $o).
tff(p10_decl, type, p10: $o).
tff(p11_decl, type, p11: $o).
tff(p12_decl, type, p12: $o).
tff(p13_decl, type, p13: $o).
tff(p14_decl, type, p14: $o).
tff(p15_decl, type, p15: $o).
tff(p16_decl, type, p16: $o).
tff(p17_decl, type, p17: $o).
tff(p18_decl, type, p18: $o).
tff(p19_decl, type, p19: $o).
tff(p2_decl, type, p2: $o).
tff(p20_decl, type, p20: $o).
tff(p21_decl, type, p21: $o).
tff(p22_decl, type, p22: $o).
tff(p23_decl, type, p23: $o).
tff(p24_decl, type, p24: $o).
tff(p25_decl, type, p25: $o).
tff(p3_decl, type, p3: $o).
tff(p30_decl, type, p30: $o).
tff(p4_decl, type, p4: $o).
tff(p5_decl, type, p5: $o).
tff(p6_decl, type, p6: $o).
tff(p7_decl, type, p7: $o).
tff(p8_decl, type, p8: $o).
tff(p9_decl, type, p9: $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_1)
& (! [W: $world, V: $world]: $accessible_world(W, V))
)).

tff(model_mapping, interpretation-mappings,
($in_world(world_0,
	(~false
	& ~p1
	& ~p10
	& ~p11
	& ~p12
	& ~p13
	& ~p14
	& ~p15
	& ~p16
	& ~p17
	& ~p18
	& ~p19
	& ~p2
	& ~p20
	& ~p21
	& ~p22
	& ~p23
	& ~p24
	& ~p25
	& ~p3
	& ~p30
	& ~p4
	& ~p5
	& ~p6
	& ~p7
	& ~p8
	& ~p9))
& $in_world(world_1,
	(~false
	& p1
	& p10
	& p11
	& p12
	& p13
	& p14
	& p15
	& p16
	& p17
	& p18
	& p19
	& p2
	& p20
	& p21
	& p22
	& p23
	& p24
	& p25
	& p3
	& p30
	& p4
	& p5
	& p6
	& p7
	& p8
	& p9))
)).