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


tff(p1001_decl, type, p1001: $o).
tff(p1002_decl, type, p1002: $o).
tff(p1003_decl, type, p1003: $o).
tff(p1004_decl, type, p1004: $o).
tff(p1005_decl, type, p1005: $o).
tff(p1006_decl, type, p1006: $o).
tff(p1007_decl, type, p1007: $o).
tff(p1008_decl, type, p1008: $o).
tff(p1009_decl, type, p1009: $o).
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(p106_decl, type, p106: $o).
tff(p107_decl, type, p107: $o).
tff(p108_decl, type, p108: $o).
tff(p109_decl, type, p109: $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(p206_decl, type, p206: $o).
tff(p207_decl, type, p207: $o).
tff(p208_decl, type, p208: $o).
tff(p209_decl, type, p209: $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(p306_decl, type, p306: $o).
tff(p307_decl, type, p307: $o).
tff(p308_decl, type, p308: $o).
tff(p309_decl, type, p309: $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(p406_decl, type, p406: $o).
tff(p407_decl, type, p407: $o).
tff(p408_decl, type, p408: $o).
tff(p409_decl, type, p409: $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(p506_decl, type, p506: $o).
tff(p507_decl, type, p507: $o).
tff(p508_decl, type, p508: $o).
tff(p509_decl, type, p509: $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(p606_decl, type, p606: $o).
tff(p607_decl, type, p607: $o).
tff(p608_decl, type, p608: $o).
tff(p609_decl, type, p609: $o).
tff(p701_decl, type, p701: $o).
tff(p702_decl, type, p702: $o).
tff(p703_decl, type, p703: $o).
tff(p704_decl, type, p704: $o).
tff(p705_decl, type, p705: $o).
tff(p706_decl, type, p706: $o).
tff(p707_decl, type, p707: $o).
tff(p708_decl, type, p708: $o).
tff(p709_decl, type, p709: $o).
tff(p801_decl, type, p801: $o).
tff(p802_decl, type, p802: $o).
tff(p803_decl, type, p803: $o).
tff(p804_decl, type, p804: $o).
tff(p805_decl, type, p805: $o).
tff(p806_decl, type, p806: $o).
tff(p807_decl, type, p807: $o).
tff(p808_decl, type, p808: $o).
tff(p809_decl, type, p809: $o).
tff(p901_decl, type, p901: $o).
tff(p902_decl, type, p902: $o).
tff(p903_decl, type, p903: $o).
tff(p904_decl, type, p904: $o).
tff(p905_decl, type, p905: $o).
tff(p906_decl, type, p906: $o).
tff(p907_decl, type, p907: $o).
tff(p908_decl, type, p908: $o).
tff(p909_decl, type, p909: $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,
	(~p1001
	& ~p1002
	& ~p1003
	& ~p1004
	& ~p1005
	& ~p1006
	& ~p1007
	& ~p1008
	& p1009
	& p101
	& ~p102
	& ~p103
	& ~p104
	& ~p105
	& ~p106
	& ~p107
	& ~p108
	& ~p109
	& ~p201
	& p202
	& ~p203
	& ~p204
	& ~p205
	& ~p206
	& ~p207
	& ~p208
	& ~p209
	& ~p301
	& ~p302
	& p303
	& ~p304
	& ~p305
	& ~p306
	& ~p307
	& ~p308
	& ~p309
	& ~p401
	& ~p402
	& ~p403
	& p404
	& ~p405
	& ~p406
	& ~p407
	& ~p408
	& ~p409
	& ~p501
	& ~p502
	& ~p503
	& ~p504
	& p505
	& ~p506
	& ~p507
	& ~p508
	& ~p509
	& ~p601
	& ~p602
	& ~p603
	& ~p604
	& ~p605
	& p606
	& ~p607
	& ~p608
	& ~p609
	& ~p701
	& ~p702
	& ~p703
	& ~p704
	& ~p705
	& ~p706
	& p707
	& ~p708
	& ~p709
	& ~p801
	& ~p802
	& ~p803
	& ~p804
	& ~p805
	& ~p806
	& p807
	& ~p808
	& ~p809
	& ~p901
	& ~p902
	& ~p903
	& ~p904
	& ~p905
	& ~p906
	& ~p907
	& p908
	& ~p909))
)).