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


tff(false_decl, type, false: $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(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(p26_decl, type, p26: $o).
tff(p31_decl, type, p31: $o).
tff(p32_decl, type, p32: $o).
tff(p33_decl, type, p33: $o).
tff(p34_decl, type, p34: $o).
tff(p35_decl, type, p35: $o).
tff(p36_decl, type, p36: $o).
tff(p41_decl, type, p41: $o).
tff(p42_decl, type, p42: $o).
tff(p43_decl, type, p43: $o).
tff(p44_decl, type, p44: $o).
tff(p45_decl, type, p45: $o).
tff(p46_decl, type, p46: $o).
tff(p51_decl, type, p51: $o).
tff(p52_decl, type, p52: $o).
tff(p53_decl, type, p53: $o).
tff(p54_decl, type, p54: $o).
tff(p55_decl, type, p55: $o).
tff(p56_decl, type, p56: $o).
tff(p61_decl, type, p61: $o).
tff(p62_decl, type, p62: $o).
tff(p63_decl, type, p63: $o).
tff(p64_decl, type, p64: $o).
tff(p65_decl, type, p65: $o).
tff(p66_decl, type, p66: $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,
	(~false
	& ~p11
	& ~p12
	& ~p13
	& p14
	& ~p15
	& p16
	& ~p21
	& p22
	& ~p23
	& p24
	& ~p25
	& p26
	& ~p31
	& p32
	& ~p33
	& p34
	& ~p35
	& ~p36
	& ~p41
	& p42
	& p43
	& p44
	& ~p45
	& p46
	& ~p51
	& p52
	& ~p53
	& p54
	& ~p55
	& p56
	& ~p61
	& p62
	& p63
	& p64
	& ~p65
	& p66))
)).