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


tff(false_decl, type, false: $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(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(p71_decl, type, p71: $o).
tff(p72_decl, type, p72: $o).
tff(p73_decl, type, p73: $o).
tff(p74_decl, type, p74: $o).
tff(p75_decl, type, p75: $o).
tff(p76_decl, type, p76: $o).
tff(p81_decl, type, p81: $o).
tff(p82_decl, type, p82: $o).
tff(p83_decl, type, p83: $o).
tff(p84_decl, type, p84: $o).
tff(p85_decl, type, p85: $o).
tff(p86_decl, type, p86: $o).
tff(p91_decl, type, p91: $o).
tff(p92_decl, type, p92: $o).
tff(p93_decl, type, p93: $o).
tff(p94_decl, type, p94: $o).
tff(p95_decl, type, p95: $o).
tff(p96_decl, type, p96: $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
	& p101
	& p102
	& ~p103
	& p104
	& ~p105
	& p106
	& ~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
	& ~p71
	& p72
	& ~p73
	& p74
	& ~p75
	& p76
	& p81
	& p82
	& ~p83
	& p84
	& ~p85
	& p86
	& ~p91
	& p92
	& ~p93
	& p94
	& ~p95
	& p96))
)).