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


tff(p101_decl, type, p101: $o).
tff(p102_decl, type, p102: $o).
tff(p103_decl, type, p103: $o).
tff(p104_decl, type, p104: $o).
tff(p105_decl, type, p105: $o).
tff(p201_decl, type, p201: $o).
tff(p202_decl, type, p202: $o).
tff(p203_decl, type, p203: $o).
tff(p204_decl, type, p204: $o).
tff(p205_decl, type, p205: $o).
tff(p301_decl, type, p301: $o).
tff(p302_decl, type, p302: $o).
tff(p303_decl, type, p303: $o).
tff(p304_decl, type, p304: $o).
tff(p305_decl, type, p305: $o).
tff(p401_decl, type, p401: $o).
tff(p402_decl, type, p402: $o).
tff(p403_decl, type, p403: $o).
tff(p404_decl, type, p404: $o).
tff(p405_decl, type, p405: $o).
tff(p501_decl, type, p501: $o).
tff(p502_decl, type, p502: $o).
tff(p503_decl, type, p503: $o).
tff(p504_decl, type, p504: $o).
tff(p505_decl, type, p505: $o).
tff(p601_decl, type, p601: $o).
tff(p602_decl, type, p602: $o).
tff(p603_decl, type, p603: $o).
tff(p604_decl, type, p604: $o).
tff(p605_decl, type, p605: $o).


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_mapping, interpretation-mappings,
($in_world(world_0,
	(p101
	& ~p102
	& ~p103
	& ~p104
	& ~p105
	& ~p201
	& p202
	& ~p203
	& ~p204
	& ~p205
	& ~p301
	& ~p302
	& p303
	& ~p304
	& ~p305
	& ~p401
	& ~p402
	& ~p403
	& p404
	& ~p405
	& ~p501
	& ~p502
	& ~p503
	& p504
	& ~p505
	& ~p601
	& ~p602
	& ~p603
	& ~p604
	& p605))
)).