1		package(load_event_b_project([event_b_model(none,'FMCH02',[sees(none,['FCTX','FCTX01','FCTX02']),refines(none,'FMCH01'),variables(none,[identifier(none,directories),identifier(none,fbuffer),identifier(none,fcontent),identifier(none,files),identifier(none,opened_files),identifier(none,parent)]),invariant(none,[member(rodinpos('FMCH02',inv1,internal_inv1I),identifier(none,fcontent),total_function(none,identifier(none,files),identifier(none,'CONTENT'))),subset(rodinpos('FMCH02',inv2,internal_inv2I),identifier(none,opened_files),identifier(none,files)),member(rodinpos('FMCH02',inv3,internal_inv3I),identifier(none,fbuffer),total_function(none,identifier(none,opened_files),identifier(none,'CONTENT')))]),theorems(none,[]),events(none,[event(rodinpos('FMCH02','INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos('FMCH02',act2,internal_act1),[identifier(none,files)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'OBJECT')))]),assign(rodinpos('FMCH02',act3,internal_act2),[identifier(none,directories)],[set_extension(none,[identifier(none,root)])]),assign(rodinpos('FMCH02',act4,internal_act5),[identifier(none,parent)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),identifier(none,'OBJECT'))))]),assign(rodinpos('FMCH02',act1,internal_act3),[identifier(none,fcontent)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'DATA'))))))]),assign(rodinpos('FMCH02',act5,internal_act4),[identifier(none,opened_files)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'OBJECT')))]),assign(rodinpos('FMCH02',act6,internal_act6),[identifier(none,fbuffer)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'DATA'))))))])],[]),event(rodinpos('FMCH02',mkdir,internal_evt2),mkdir,ordinary(none),[mkdir],[identifier(rodinpos('FMCH02',[],internal_var3),indr),identifier(rodinpos('FMCH02',[],internal_var1),obj)],[member(rodinpos('FMCH02',grd1,internal_grd1),identifier(none,obj),set_subtraction(none,identifier(none,'OBJECT'),union(none,identifier(none,files),identifier(none,directories)))),member(rodinpos('FMCH02',grd2,internal_grd3),identifier(none,indr),identifier(none,directories))],[],[assign(rodinpos('FMCH02',act2,internal_act2),[identifier(none,directories)],[union(none,identifier(none,directories),set_extension(none,[identifier(none,obj)]))]),assign(rodinpos('FMCH02',act3,internal_act4),[identifier(none,parent)],[overwrite(none,identifier(none,parent),set_extension(none,[couple(none,[identifier(none,obj),identifier(none,indr)])]))])],[]),event(rodinpos('FMCH02',crt_file,internal_evt3),crt_file,ordinary(none),[crt_file],[identifier(rodinpos('FMCH02',[],internal_var3),indr),identifier(rodinpos('FMCH02',[],internal_var1),obj)],[member(rodinpos('FMCH02',grd1,internal_grd1),identifier(none,obj),set_subtraction(none,identifier(none,'OBJECT'),union(none,identifier(none,files),identifier(none,directories)))),member(rodinpos('FMCH02',grd2,internal_grd3),identifier(none,indr),identifier(none,directories))],[],[assign(rodinpos('FMCH02',act2,internal_act2),[identifier(none,files)],[union(none,identifier(none,files),set_extension(none,[identifier(none,obj)]))]),assign(rodinpos('FMCH02',act3,internal_act4),[identifier(none,parent)],[overwrite(none,identifier(none,parent),set_extension(none,[couple(none,[identifier(none,obj),identifier(none,indr)])]))]),assign(rodinpos('FMCH02',act1,internal_act1),[identifier(none,fcontent)],[overwrite(none,identifier(none,fcontent),set_extension(none,[couple(none,[identifier(none,obj),typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'DATA'))))])]))])],[]),event(rodinpos('FMCH02',move,internal_evt5),move,ordinary(none),[move],[identifier(rodinpos('FMCH02',[],internal_var4),des),identifier(rodinpos('FMCH02',[],internal_var1),obj),identifier(rodinpos('FMCH02',[],internal_var3),to)],[member(rodinpos('FMCH02',grd1,internal_grd1),identifier(none,obj),set_subtraction(none,union(none,identifier(none,files),identifier(none,directories)),set_extension(none,[identifier(none,root)]))),member(rodinpos('FMCH02',grd3,internal_grd3),identifier(none,to),identifier(none,directories)),equal(rodinpos('FMCH02',grd6,internal_grd5),identifier(none,des),image(none,reverse(none,function(none,identifier(none,tcl),[identifier(none,parent)])),set_extension(none,[identifier(none,obj)]))),not_member(rodinpos('FMCH02',grd7,internal_grd6),identifier(none,to),union(none,identifier(none,des),set_extension(none,[identifier(none,obj)])))],[],[assign(rodinpos('FMCH02',act1,internal_act1),[identifier(none,parent)],[overwrite(none,identifier(none,parent),set_extension(none,[couple(none,[identifier(none,obj),identifier(none,to)])]))])],[]),event(rodinpos('FMCH02',delete,evt2),delete,ordinary(none),[delete],[identifier(rodinpos('FMCH02',[],internal_var3),des),identifier(rodinpos('FMCH02',[],internal_var1),obj),identifier(rodinpos('FMCH02',[],internal_element1),objs)],[member(rodinpos('FMCH02',grd1,internal_grd1),identifier(none,obj),set_subtraction(none,union(none,identifier(none,files),identifier(none,directories)),set_extension(none,[identifier(none,root)]))),subset(rodinpos('FMCH02',grd4,internal_grd4),identifier(none,des),union(none,identifier(none,files),identifier(none,directories))),equal(rodinpos('FMCH02',grd6,internal_grd6),identifier(none,des),image(none,reverse(none,function(none,identifier(none,tcl),[identifier(none,parent)])),set_extension(none,[identifier(none,obj)]))),equal(rodinpos('FMCH02',grd5,internal_element1),identifier(none,objs),union(none,identifier(none,des),set_extension(none,[identifier(none,obj)]))),equal(rodinpos('FMCH02',grd2,internal_element2),intersection(none,identifier(none,objs),identifier(none,opened_files)),typeof(none,empty_set(none),pow_subset(none,identifier(none,'OBJECT'))))],[],[assign(rodinpos('FMCH02',act4,internal_act4),[identifier(none,parent)],[domain_subtraction(none,identifier(none,objs),identifier(none,parent))]),assign(rodinpos('FMCH02',act2,internal_act2),[identifier(none,files)],[set_subtraction(none,identifier(none,files),intersection(none,identifier(none,objs),identifier(none,files)))]),assign(rodinpos('FMCH02',act3,internal_act3),[identifier(none,directories)],[set_subtraction(none,identifier(none,directories),intersection(none,identifier(none,objs),identifier(none,directories)))]),assign(rodinpos('FMCH02',act1,internal_act1),[identifier(none,fcontent)],[domain_subtraction(none,intersection(none,identifier(none,objs),identifier(none,files)),identifier(none,fcontent))])],[]),event(rodinpos('FMCH02',copy,evt0),copy,ordinary(none),[copy],[identifier(rodinpos('FMCH02',[],internal_var6),corres),identifier(rodinpos('FMCH02',[],internal_element1),des),identifier(rodinpos('FMCH02',[],internal_element3),nobj),identifier(rodinpos('FMCH02',[],internal_element2),nobjs),identifier(rodinpos('FMCH02',[],internal_var1),obj),identifier(rodinpos('FMCH02',[],internal_var4),objs),identifier(rodinpos('FMCH02',[],internal_element5),replica),identifier(rodinpos('FMCH02',[],internal_element4),subparent),identifier(rodinpos('FMCH02',[],internal_var3),to)],[member(rodinpos('FMCH02',grd1,internal_grd1),identifier(none,obj),set_subtraction(none,union(none,identifier(none,files),identifier(none,directories)),set_extension(none,[identifier(none,root)]))),subset(rodinpos('FMCH02',grd9,internal_grd2),identifier(none,des),union(none,identifier(none,files),identifier(none,directories))),equal(rodinpos('FMCH02',grd7,element0),identifier(none,des),image(none,reverse(none,function(none,identifier(none,tcl),[identifier(none,parent)])),set_extension(none,[identifier(none,obj)]))),member(rodinpos('FMCH02',grd3,internal_grd3),identifier(none,to),identifier(none,directories)),not_member(rodinpos('FMCH02',grd11,internal_grd11),identifier(none,to),union(none,identifier(none,des),set_extension(none,[identifier(none,obj)]))),equal(rodinpos('FMCH02',grd6,internal_element2),identifier(none,objs),union(none,identifier(none,des),set_extension(none,[identifier(none,obj)]))),subset(rodinpos('FMCH02',grd5,internal_grd5),identifier(none,nobjs),set_subtraction(none,identifier(none,'OBJECT'),union(none,identifier(none,files),identifier(none,directories)))),member(rodinpos('FMCH02',grd10,internal_grd9),identifier(none,corres),total_bijection(none,identifier(none,objs),identifier(none,nobjs))),equal(rodinpos('FMCH02',grd2,internal_element1),identifier(none,nobj),function(none,identifier(none,corres),[identifier(none,obj)])),equal(rodinpos('FMCH02',grd4,internal_element3),identifier(none,subparent),domain_restriction(none,identifier(none,des),identifier(none,parent))),equal(rodinpos('FMCH02',grd8,internal_element4),identifier(none,replica),composition(none,reverse(none,identifier(none,corres)),composition(none,identifier(none,subparent),identifier(none,corres))))],[],[assign(rodinpos('FMCH02',act1,internal_act1),[identifier(none,parent)],[union(none,identifier(none,parent),union(none,identifier(none,replica),set_extension(none,[couple(none,[identifier(none,nobj),identifier(none,to)])])))]),assign(rodinpos('FMCH02',act3,element1),[identifier(none,files)],[union(none,identifier(none,files),image(none,identifier(none,corres),intersection(none,identifier(none,objs),identifier(none,files))))]),assign(rodinpos('FMCH02',act4,element2),[identifier(none,directories)],[union(none,identifier(none,directories),image(none,identifier(none,corres),intersection(none,identifier(none,objs),identifier(none,directories))))]),assign(rodinpos('FMCH02',act2,internal_act2),[identifier(none,fcontent)],[union(none,identifier(none,fcontent),composition(none,reverse(none,identifier(none,corres)),identifier(none,fcontent)))])],[]),event(rodinpos('FMCH02',readfile,internal_evt4),readfile,ordinary(none),[],[identifier(rodinpos('FMCH02',[],internal_var1),f)],[member(rodinpos('FMCH02',grd1,internal_grd1),identifier(none,f),identifier(none,opened_files))],[],[assign(rodinpos('FMCH02',act1,internal_act1),[identifier(none,fbuffer)],[overwrite(none,identifier(none,fbuffer),set_extension(none,[couple(none,[identifier(none,f),function(none,identifier(none,fcontent),[identifier(none,f)])])]))])],[]),event(rodinpos('FMCH02',writefile,internal_evt6),writefile,ordinary(none),[],[identifier(rodinpos('FMCH02',[],internal_var1),f)],[member(rodinpos('FMCH02',grd1,internal_grd1),identifier(none,f),identifier(none,opened_files))],[],[assign(rodinpos('FMCH02',act1,internal_act1),[identifier(none,fcontent)],[overwrite(none,identifier(none,fcontent),set_extension(none,[couple(none,[identifier(none,f),function(none,identifier(none,fbuffer),[identifier(none,f)])])]))])],[]),event(rodinpos('FMCH02',open,internal_evt7),open,ordinary(none),[],[identifier(rodinpos('FMCH02',[],internal_var1),f)],[member(rodinpos('FMCH02',grd1,internal_grd1),identifier(none,f),identifier(none,files)),not_member(rodinpos('FMCH02',grd2,internal_grd2),identifier(none,f),identifier(none,opened_files))],[],[assign(rodinpos('FMCH02',act1,internal_act1),[identifier(none,opened_files)],[union(none,identifier(none,opened_files),set_extension(none,[identifier(none,f)]))]),assign(rodinpos('FMCH02',act2,internal_act2),[identifier(none,fbuffer)],[overwrite(none,identifier(none,fbuffer),set_extension(none,[couple(none,[identifier(none,f),typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'DATA'))))])]))])],[]),event(rodinpos('FMCH02',close,internal_evt8),close,ordinary(none),[],[identifier(rodinpos('FMCH02',[],internal_var1),f)],[member(rodinpos('FMCH02',grd1,internal_grd1),identifier(none,f),identifier(none,opened_files))],[],[assign(rodinpos('FMCH02',act1,internal_act1),[identifier(none,opened_files)],[set_subtraction(none,identifier(none,opened_files),set_extension(none,[identifier(none,f)]))]),assign(rodinpos('FMCH02',act2,internal_act2),[identifier(none,fbuffer)],[domain_subtraction(none,set_extension(none,[identifier(none,f)]),identifier(none,fbuffer))])],[])])]),event_b_model(none,'FMCH01',[sees(none,['FCTX','FCTX01']),refines(none,'FMCH00'),variables(none,[identifier(none,directories),identifier(none,files),identifier(none,parent)]),invariant(none,[subset(rodinpos('FMCH01',inv2,internal_inv1I),identifier(none,files),identifier(none,objects)),subset(rodinpos('FMCH01',inv3,internal_inv2I),identifier(none,directories),identifier(none,objects)),equal(rodinpos('FMCH01',inv4,internal_inv4I),intersection(none,identifier(none,files),identifier(none,directories)),typeof(none,empty_set(none),pow_subset(none,identifier(none,'OBJECT')))),equal(rodinpos('FMCH01',inv5,internal_inv5I),identifier(none,objects),union(none,identifier(none,files),identifier(none,directories))),member(rodinpos('FMCH01',inv6,internal_inv6I),identifier(none,root),identifier(none,directories)),subset(rodinpos('FMCH01',inv1,internal_inv3I),range(none,identifier(none,parent)),identifier(none,directories))]),theorems(none,[]),events(none,[event(rodinpos('FMCH01','INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos('FMCH01',act2,internal_act1),[identifier(none,files)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'OBJECT')))]),assign(rodinpos('FMCH01',act3,internal_act2),[identifier(none,directories)],[set_extension(none,[identifier(none,root)])]),assign(rodinpos('FMCH01',act4,internal_act5),[identifier(none,parent)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),identifier(none,'OBJECT'))))])],[]),event(rodinpos('FMCH01',mkdir,internal_evt2),mkdir,ordinary(none),[newobj],[identifier(rodinpos('FMCH01',[],internal_var3),indr),identifier(rodinpos('FMCH01',[],internal_var1),obj)],[member(rodinpos('FMCH01',grd1,internal_grd1),identifier(none,obj),set_subtraction(none,identifier(none,'OBJECT'),union(none,identifier(none,files),identifier(none,directories)))),member(rodinpos('FMCH01',grd2,internal_grd3),identifier(none,indr),identifier(none,directories))],[],[assign(rodinpos('FMCH01',act2,internal_act2),[identifier(none,directories)],[union(none,identifier(none,directories),set_extension(none,[identifier(none,obj)]))]),assign(rodinpos('FMCH01',act3,internal_act4),[identifier(none,parent)],[overwrite(none,identifier(none,parent),set_extension(none,[couple(none,[identifier(none,obj),identifier(none,indr)])]))])],[]),event(rodinpos('FMCH01',crt_file,internal_evt3),crt_file,ordinary(none),[newobj],[identifier(rodinpos('FMCH01',[],internal_var3),indr),identifier(rodinpos('FMCH01',[],internal_var1),obj)],[member(rodinpos('FMCH01',grd1,internal_grd1),identifier(none,obj),set_subtraction(none,identifier(none,'OBJECT'),union(none,identifier(none,files),identifier(none,directories)))),member(rodinpos('FMCH01',grd2,internal_grd3),identifier(none,indr),identifier(none,directories))],[],[assign(rodinpos('FMCH01',act2,internal_act2),[identifier(none,files)],[union(none,identifier(none,files),set_extension(none,[identifier(none,obj)]))]),assign(rodinpos('FMCH01',act3,internal_act4),[identifier(none,parent)],[overwrite(none,identifier(none,parent),set_extension(none,[couple(none,[identifier(none,obj),identifier(none,indr)])]))])],[]),event(rodinpos('FMCH01',move,internal_evt5),move,ordinary(none),[move],[identifier(rodinpos('FMCH01',[],internal_var4),des),identifier(rodinpos('FMCH01',[],internal_var1),obj),identifier(rodinpos('FMCH01',[],internal_var3),to)],[member(rodinpos('FMCH01',grd1,internal_grd1),identifier(none,obj),set_subtraction(none,union(none,identifier(none,files),identifier(none,directories)),set_extension(none,[identifier(none,root)]))),member(rodinpos('FMCH01',grd3,internal_grd3),identifier(none,to),identifier(none,directories)),equal(rodinpos('FMCH01',grd6,internal_grd5),identifier(none,des),image(none,reverse(none,function(none,identifier(none,tcl),[identifier(none,parent)])),set_extension(none,[identifier(none,obj)]))),not_member(rodinpos('FMCH01',grd7,internal_grd6),identifier(none,to),union(none,identifier(none,des),set_extension(none,[identifier(none,obj)])))],[],[assign(rodinpos('FMCH01',act1,internal_act1),[identifier(none,parent)],[overwrite(none,identifier(none,parent),set_extension(none,[couple(none,[identifier(none,obj),identifier(none,to)])]))])],[]),event(rodinpos('FMCH01',delete,evt2),delete,ordinary(none),[delete],[identifier(rodinpos('FMCH01',[],internal_var3),des),identifier(rodinpos('FMCH01',[],internal_var1),obj),identifier(rodinpos('FMCH01',[],internal_element1),objs)],[member(rodinpos('FMCH01',grd1,internal_grd1),identifier(none,obj),set_subtraction(none,union(none,identifier(none,files),identifier(none,directories)),set_extension(none,[identifier(none,root)]))),subset(rodinpos('FMCH01',grd4,internal_grd4),identifier(none,des),union(none,identifier(none,files),identifier(none,directories))),equal(rodinpos('FMCH01',grd6,internal_grd6),identifier(none,des),image(none,reverse(none,function(none,identifier(none,tcl),[identifier(none,parent)])),set_extension(none,[identifier(none,obj)]))),equal(rodinpos('FMCH01',grd5,internal_element1),identifier(none,objs),union(none,identifier(none,des),set_extension(none,[identifier(none,obj)])))],[],[assign(rodinpos('FMCH01',act4,internal_act4),[identifier(none,parent)],[domain_subtraction(none,identifier(none,objs),identifier(none,parent))]),assign(rodinpos('FMCH01',act2,internal_act2),[identifier(none,files)],[set_subtraction(none,identifier(none,files),intersection(none,identifier(none,objs),identifier(none,files)))]),assign(rodinpos('FMCH01',act3,internal_act3),[identifier(none,directories)],[set_subtraction(none,identifier(none,directories),intersection(none,identifier(none,objs),identifier(none,directories)))])],[]),event(rodinpos('FMCH01',copy,evt0),copy,ordinary(none),[copy],[identifier(rodinpos('FMCH01',[],internal_var6),corres),identifier(rodinpos('FMCH01',[],internal_element1),des),identifier(rodinpos('FMCH01',[],internal_element3),nobj),identifier(rodinpos('FMCH01',[],internal_element2),nobjs),identifier(rodinpos('FMCH01',[],internal_var1),obj),identifier(rodinpos('FMCH01',[],internal_var4),objs),identifier(rodinpos('FMCH01',[],internal_element5),replica),identifier(rodinpos('FMCH01',[],internal_element4),subparent),identifier(rodinpos('FMCH01',[],internal_var3),to)],[member(rodinpos('FMCH01',grd1,internal_grd1),identifier(none,obj),set_subtraction(none,union(none,identifier(none,files),identifier(none,directories)),set_extension(none,[identifier(none,root)]))),subset(rodinpos('FMCH01',grd9,internal_grd2),identifier(none,des),union(none,identifier(none,files),identifier(none,directories))),equal(rodinpos('FMCH01',grd7,element0),identifier(none,des),image(none,reverse(none,function(none,identifier(none,tcl),[identifier(none,parent)])),set_extension(none,[identifier(none,obj)]))),member(rodinpos('FMCH01',grd3,internal_grd3),identifier(none,to),identifier(none,directories)),not_member(rodinpos('FMCH01',grd11,internal_grd11),identifier(none,to),union(none,identifier(none,des),set_extension(none,[identifier(none,obj)]))),equal(rodinpos('FMCH01',grd6,internal_element2),identifier(none,objs),union(none,identifier(none,des),set_extension(none,[identifier(none,obj)]))),subset(rodinpos('FMCH01',grd5,internal_grd5),identifier(none,nobjs),set_subtraction(none,identifier(none,'OBJECT'),union(none,identifier(none,files),identifier(none,directories)))),member(rodinpos('FMCH01',grd10,internal_grd9),identifier(none,corres),total_bijection(none,identifier(none,objs),identifier(none,nobjs))),equal(rodinpos('FMCH01',grd2,internal_element1),identifier(none,nobj),function(none,identifier(none,corres),[identifier(none,obj)])),equal(rodinpos('FMCH01',grd4,internal_element3),identifier(none,subparent),domain_restriction(none,identifier(none,des),identifier(none,parent))),equal(rodinpos('FMCH01',grd8,internal_element4),identifier(none,replica),composition(none,reverse(none,identifier(none,corres)),composition(none,identifier(none,subparent),identifier(none,corres))))],[],[assign(rodinpos('FMCH01',act1,internal_act1),[identifier(none,parent)],[union(none,identifier(none,parent),union(none,identifier(none,replica),set_extension(none,[couple(none,[identifier(none,nobj),identifier(none,to)])])))]),assign(rodinpos('FMCH01',act3,element1),[identifier(none,files)],[union(none,identifier(none,files),image(none,identifier(none,corres),intersection(none,identifier(none,objs),identifier(none,files))))]),assign(rodinpos('FMCH01',act4,element2),[identifier(none,directories)],[union(none,identifier(none,directories),image(none,identifier(none,corres),intersection(none,identifier(none,objs),identifier(none,directories))))])],[])])]),event_b_model(none,'FMCH00',[sees(none,['FCTX','FCTX01']),variables(none,[identifier(none,objects),identifier(none,parent)]),invariant(none,[member(rodinpos('FMCH00',inv1,internal_inv3I),identifier(none,objects),pow_subset(none,identifier(none,'OBJECT'))),member(rodinpos('FMCH00',inv6,internal_inv6I),identifier(none,root),identifier(none,objects)),member(rodinpos('FMCH00',inv8,internal_inv7I),identifier(none,parent),total_function(none,set_subtraction(none,identifier(none,objects),set_extension(none,[identifier(none,root)])),identifier(none,objects))),forall(rodinpos('FMCH00',inv10,internal_inv9I),[identifier(none,s)],implication(none,conjunct(none,member(none,identifier(none,s),pow_subset(none,identifier(none,'OBJECT'))),subset(none,identifier(none,s),image(none,reverse(none,identifier(none,parent)),identifier(none,s)))),equal(none,identifier(none,s),typeof(none,empty_set(none),pow_subset(none,identifier(none,'OBJECT'))))))]),theorems(none,[equal(rodinpos('FMCH00',thm1,internal_thm1T),intersection(none,function(none,identifier(none,tcl),[identifier(none,parent)]),domain_restriction(none,identifier(none,'OBJECT'),typeof(none,event_b_identity(none),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),identifier(none,'OBJECT')))))),typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),identifier(none,'OBJECT'))))),forall(rodinpos('FMCH00',thm3,internal_element2T),[identifier(none,'T')],implication(none,conjunct(none,member(none,identifier(none,'T'),pow_subset(none,identifier(none,'OBJECT'))),conjunct(none,member(none,identifier(none,root),identifier(none,'T')),subset(none,image(none,reverse(none,identifier(none,parent)),identifier(none,'T')),identifier(none,'T')))),subset(none,identifier(none,objects),identifier(none,'T')))),subset(rodinpos('FMCH00',thm4,internal_element3T),identifier(none,objects),union(none,set_extension(none,[identifier(none,root)]),image(none,reverse(none,function(none,identifier(none,tcl),[identifier(none,parent)])),set_extension(none,[identifier(none,root)])))),subset(rodinpos('FMCH00',thm2,internal_element1T),set_subtraction(none,identifier(none,objects),set_extension(none,[identifier(none,root)])),image(none,reverse(none,function(none,identifier(none,tcl),[identifier(none,parent)])),set_extension(none,[identifier(none,root)]))),forall(rodinpos('FMCH00',thm5,internal_thm2T),[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),identifier(none,'OBJECT')),not_member(none,identifier(none,x),range(none,identifier(none,parent)))),equal(none,image(none,reverse(none,function(none,identifier(none,tcl),[identifier(none,parent)])),set_extension(none,[identifier(none,x)])),typeof(none,empty_set(none),pow_subset(none,identifier(none,'OBJECT')))))),forall(rodinpos('FMCH00',thm6,internal_thm3T),[identifier(none,x)],implication(none,member(none,identifier(none,x),identifier(none,'OBJECT')),member(none,domain_restriction(none,image(none,reverse(none,function(none,identifier(none,tcl),[identifier(none,parent)])),set_extension(none,[identifier(none,x)])),identifier(none,parent)),total_function(none,image(none,reverse(none,function(none,identifier(none,tcl),[identifier(none,parent)])),set_extension(none,[identifier(none,x)])),union(none,image(none,reverse(none,function(none,identifier(none,tcl),[identifier(none,parent)])),set_extension(none,[identifier(none,x)])),set_extension(none,[identifier(none,x)])))))),forall(rodinpos('FMCH00',thm7,internal_thm4T),[identifier(none,x)],implication(none,member(none,identifier(none,x),identifier(none,'OBJECT')),member(none,domain_restriction(none,image(none,reverse(none,function(none,identifier(none,tcl),[identifier(none,parent)])),set_extension(none,[identifier(none,x)])),identifier(none,parent)),total_function(none,set_subtraction(none,union(none,image(none,reverse(none,function(none,identifier(none,tcl),[identifier(none,parent)])),set_extension(none,[identifier(none,x)])),set_extension(none,[identifier(none,x)])),set_extension(none,[identifier(none,x)])),union(none,image(none,reverse(none,function(none,identifier(none,tcl),[identifier(none,parent)])),set_extension(none,[identifier(none,x)])),set_extension(none,[identifier(none,x)])))))),forall(rodinpos('FMCH00',thm8,internal_thm5T),[identifier(none,x),identifier(none,s)],implication(none,conjunct(none,member(none,identifier(none,x),identifier(none,'OBJECT')),conjunct(none,member(none,identifier(none,s),pow_subset(none,identifier(none,'OBJECT'))),subset(none,identifier(none,s),image(none,reverse(none,domain_restriction(none,image(none,reverse(none,function(none,identifier(none,tcl),[identifier(none,parent)])),set_extension(none,[identifier(none,x)])),identifier(none,parent))),identifier(none,s))))),equal(none,identifier(none,s),typeof(none,empty_set(none),pow_subset(none,identifier(none,'OBJECT')))))),forall(rodinpos('FMCH00',thm9,internal_element4T),[identifier(none,x)],implication(none,member(none,identifier(none,x),identifier(none,'OBJECT')),member(none,domain_subtraction(none,union(none,image(none,reverse(none,function(none,identifier(none,tcl),[identifier(none,parent)])),set_extension(none,[identifier(none,x)])),set_extension(none,[identifier(none,x)])),identifier(none,parent)),total_function(none,set_subtraction(none,set_subtraction(none,identifier(none,objects),union(none,image(none,reverse(none,function(none,identifier(none,tcl),[identifier(none,parent)])),set_extension(none,[identifier(none,x)])),set_extension(none,[identifier(none,x)]))),set_extension(none,[identifier(none,root)])),set_subtraction(none,identifier(none,objects),union(none,image(none,reverse(none,function(none,identifier(none,tcl),[identifier(none,parent)])),set_extension(none,[identifier(none,x)])),set_extension(none,[identifier(none,x)])))))))]),events(none,[event(rodinpos('FMCH00','INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos('FMCH00',act1,internal_act3),[identifier(none,objects)],[set_extension(none,[identifier(none,root)])]),assign(rodinpos('FMCH00',act4,internal_act5),[identifier(none,parent)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),identifier(none,'OBJECT'))))])],[]),event(rodinpos('FMCH00',newobj,internal_evt2),newobj,ordinary(none),[],[identifier(rodinpos('FMCH00',[],internal_var3),indr),identifier(rodinpos('FMCH00',[],internal_var1),obj)],[member(rodinpos('FMCH00',grd1,internal_grd1),identifier(none,obj),set_subtraction(none,identifier(none,'OBJECT'),identifier(none,objects))),member(rodinpos('FMCH00',grd2,internal_grd3),identifier(none,indr),identifier(none,objects))],[],[assign(rodinpos('FMCH00',act1,internal_act1),[identifier(none,objects)],[union(none,identifier(none,objects),set_extension(none,[identifier(none,obj)]))]),assign(rodinpos('FMCH00',act3,internal_act4),[identifier(none,parent)],[overwrite(none,identifier(none,parent),set_extension(none,[couple(none,[identifier(none,obj),identifier(none,indr)])]))])],[]),event(rodinpos('FMCH00',move,internal_evt5),move,ordinary(none),[],[identifier(rodinpos('FMCH00',[],internal_var4),des),identifier(rodinpos('FMCH00',[],internal_var1),obj),identifier(rodinpos('FMCH00',[],internal_var3),to)],[member(rodinpos('FMCH00',grd1,internal_grd1),identifier(none,obj),set_subtraction(none,identifier(none,objects),set_extension(none,[identifier(none,root)]))),member(rodinpos('FMCH00',grd3,internal_grd3),identifier(none,to),identifier(none,objects)),equal(rodinpos('FMCH00',grd6,internal_grd5),identifier(none,des),image(none,reverse(none,function(none,identifier(none,tcl),[identifier(none,parent)])),set_extension(none,[identifier(none,obj)]))),not_member(rodinpos('FMCH00',grd7,internal_grd6),identifier(none,to),union(none,identifier(none,des),set_extension(none,[identifier(none,obj)])))],[],[assign(rodinpos('FMCH00',act1,internal_act1),[identifier(none,parent)],[overwrite(none,identifier(none,parent),set_extension(none,[couple(none,[identifier(none,obj),identifier(none,to)])]))])],[]),event(rodinpos('FMCH00',delete,evt2),delete,ordinary(none),[],[identifier(rodinpos('FMCH00',[],internal_var3),des),identifier(rodinpos('FMCH00',[],internal_var1),obj),identifier(rodinpos('FMCH00',[],internal_element1),objs)],[member(rodinpos('FMCH00',grd1,internal_grd1),identifier(none,obj),set_subtraction(none,identifier(none,objects),set_extension(none,[identifier(none,root)]))),subset(rodinpos('FMCH00',grd4,internal_grd4),identifier(none,des),identifier(none,objects)),equal(rodinpos('FMCH00',grd6,internal_grd6),identifier(none,des),image(none,reverse(none,function(none,identifier(none,tcl),[identifier(none,parent)])),set_extension(none,[identifier(none,obj)]))),equal(rodinpos('FMCH00',grd5,internal_element1),identifier(none,objs),union(none,identifier(none,des),set_extension(none,[identifier(none,obj)])))],[],[assign(rodinpos('FMCH00',act1,internal_act1),[identifier(none,objects)],[set_subtraction(none,identifier(none,objects),identifier(none,objs))]),assign(rodinpos('FMCH00',act4,internal_act4),[identifier(none,parent)],[domain_subtraction(none,identifier(none,objs),identifier(none,parent))])],[]),event(rodinpos('FMCH00',copy,internal_evt6),copy,ordinary(none),[],[identifier(rodinpos('FMCH00',[],internal_var6),corres),identifier(rodinpos('FMCH00',[],internal_element1),des),identifier(rodinpos('FMCH00',[],internal_element3),nobj),identifier(rodinpos('FMCH00',[],internal_element2),nobjs),identifier(rodinpos('FMCH00',[],internal_var1),obj),identifier(rodinpos('FMCH00',[],internal_var4),objs),identifier(rodinpos('FMCH00',[],internal_element5),replica),identifier(rodinpos('FMCH00',[],internal_element4),subparent),identifier(rodinpos('FMCH00',[],internal_var3),to)],[member(rodinpos('FMCH00',grd1,internal_grd1),identifier(none,obj),set_subtraction(none,identifier(none,objects),set_extension(none,[identifier(none,root)]))),subset(rodinpos('FMCH00',grd9,internal_grd2),identifier(none,des),identifier(none,objects)),equal(rodinpos('FMCH00',grd7,element0),identifier(none,des),image(none,reverse(none,function(none,identifier(none,tcl),[identifier(none,parent)])),set_extension(none,[identifier(none,obj)]))),member(rodinpos('FMCH00',grd3,internal_grd3),identifier(none,to),identifier(none,objects)),not_member(rodinpos('FMCH00',grd11,internal_grd11),identifier(none,to),union(none,identifier(none,des),set_extension(none,[identifier(none,obj)]))),equal(rodinpos('FMCH00',grd6,internal_element2),identifier(none,objs),union(none,identifier(none,des),set_extension(none,[identifier(none,obj)]))),subset(rodinpos('FMCH00',grd5,internal_grd5),identifier(none,nobjs),set_subtraction(none,identifier(none,'OBJECT'),identifier(none,objects))),member(rodinpos('FMCH00',grd10,internal_grd9),identifier(none,corres),total_bijection(none,identifier(none,objs),identifier(none,nobjs))),equal(rodinpos('FMCH00',grd2,internal_element1),identifier(none,nobj),function(none,identifier(none,corres),[identifier(none,obj)])),equal(rodinpos('FMCH00',grd4,internal_element3),identifier(none,subparent),domain_restriction(none,identifier(none,des),identifier(none,parent))),equal(rodinpos('FMCH00',grd8,internal_element4),identifier(none,replica),composition(none,reverse(none,identifier(none,corres)),composition(none,identifier(none,subparent),identifier(none,corres))))],[],[assign(rodinpos('FMCH00',act1,internal_act1),[identifier(none,parent)],[union(none,identifier(none,parent),union(none,identifier(none,replica),set_extension(none,[couple(none,[identifier(none,nobj),identifier(none,to)])])))]),assign(rodinpos('FMCH00',act2,internal_act2),[identifier(none,objects)],[union(none,identifier(none,objects),identifier(none,nobjs))])],[])])])],[event_b_context(none,'FCTX',[extends(none,[]),constants(none,[identifier(none,objfn),identifier(none,objrel),identifier(none,root),identifier(none,tcl)]),abstract_constants(none,[]),axioms(none,[member(rodinpos('FCTX',axm1,internal_axm1A),identifier(none,root),identifier(none,'OBJECT')),equal(rodinpos('FCTX',axm2,internal_axm4A),identifier(none,objfn),partial_function(none,set_subtraction(none,identifier(none,'OBJECT'),set_extension(none,[identifier(none,root)])),identifier(none,'OBJECT'))),equal(rodinpos('FCTX',axm4,internal_axm2A),identifier(none,objrel),relations(none,identifier(none,'OBJECT'),identifier(none,'OBJECT'))),member(rodinpos('FCTX',axm3,internal_axm3A),identifier(none,tcl),total_function(none,identifier(none,objrel),identifier(none,objrel))),forall(rodinpos('FCTX',axm5,internal_axm7A),[identifier(none,r)],implication(none,conjunct(none,member(none,identifier(none,r),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),identifier(none,'OBJECT')))),member(none,identifier(none,r),identifier(none,objrel))),subset(none,identifier(none,r),function(none,identifier(none,tcl),[identifier(none,r)])))),forall(rodinpos('FCTX',axm6,internal_axm8A),[identifier(none,r)],implication(none,conjunct(none,member(none,identifier(none,r),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),identifier(none,'OBJECT')))),member(none,identifier(none,r),identifier(none,objrel))),subset(none,composition(none,identifier(none,r),function(none,identifier(none,tcl),[identifier(none,r)])),function(none,identifier(none,tcl),[identifier(none,r)])))),forall(rodinpos('FCTX',axm7,internal_axm11A),[identifier(none,r),identifier(none,t)],implication(none,conjunct(none,member(none,identifier(none,r),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),identifier(none,'OBJECT')))),conjunct(none,member(none,identifier(none,t),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),identifier(none,'OBJECT')))),conjunct(none,member(none,identifier(none,r),identifier(none,objrel)),conjunct(none,subset(none,identifier(none,r),identifier(none,t)),subset(none,composition(none,identifier(none,r),identifier(none,t)),identifier(none,t)))))),subset(none,function(none,identifier(none,tcl),[identifier(none,r)]),identifier(none,t))))]),theorems(none,[subset(rodinpos('FCTX',thm5,internal_thm8T),identifier(none,objfn),identifier(none,objrel)),forall(rodinpos('FCTX',thm1,internal_thm2T),[identifier(none,r)],implication(none,conjunct(none,member(none,identifier(none,r),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),identifier(none,'OBJECT')))),member(none,identifier(none,r),identifier(none,objrel))),equal(none,function(none,identifier(none,tcl),[identifier(none,r)]),union(none,identifier(none,r),composition(none,identifier(none,r),function(none,identifier(none,tcl),[identifier(none,r)])))))),truth(rodinpos('FCTX',thm4,internal_thm4T)),forall(rodinpos('FCTX',thm2,internal_thm1T),[identifier(none,t)],implication(none,conjunct(none,member(none,identifier(none,t),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),identifier(none,'OBJECT')))),conjunct(none,member(none,identifier(none,t),identifier(none,objfn)),forall(none,[identifier(none,s)],implication(none,conjunct(none,member(none,identifier(none,s),pow_subset(none,identifier(none,'OBJECT'))),subset(none,identifier(none,s),image(none,reverse(none,identifier(none,t)),identifier(none,s)))),equal(none,identifier(none,s),typeof(none,empty_set(none),pow_subset(none,identifier(none,'OBJECT')))))))),equal(none,intersection(none,function(none,identifier(none,tcl),[identifier(none,t)]),domain_restriction(none,identifier(none,'OBJECT'),typeof(none,event_b_identity(none),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),identifier(none,'OBJECT')))))),typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),identifier(none,'OBJECT'))))))),equal(rodinpos('FCTX',thm3,internal_thm3T),function(none,identifier(none,tcl),[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),identifier(none,'OBJECT'))))]),typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),identifier(none,'OBJECT')))))]),sets(none,[deferred_set(none,'OBJECT')])]),event_b_context(none,'FCTX01',[extends(none,['FCTX']),constants(none,[]),abstract_constants(none,[]),axioms(none,[]),theorems(none,[forall(rodinpos('FCTX01',thm1,internal_element1T),[identifier(none,r),identifier(none,r2)],implication(none,conjunct(none,member(none,identifier(none,r),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),identifier(none,'OBJECT')))),conjunct(none,member(none,identifier(none,r2),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),identifier(none,'OBJECT')))),conjunct(none,member(none,identifier(none,r),identifier(none,objrel)),conjunct(none,member(none,identifier(none,r2),identifier(none,objrel)),conjunct(none,subset(none,identifier(none,r2),identifier(none,r)),forall(none,[identifier(none,s)],implication(none,conjunct(none,member(none,identifier(none,s),pow_subset(none,identifier(none,'OBJECT'))),subset(none,identifier(none,s),image(none,identifier(none,r),identifier(none,s)))),equal(none,identifier(none,s),typeof(none,empty_set(none),pow_subset(none,identifier(none,'OBJECT'))))))))))),forall(none,[identifier(none,t)],implication(none,conjunct(none,member(none,identifier(none,t),pow_subset(none,identifier(none,'OBJECT'))),subset(none,identifier(none,t),image(none,identifier(none,r2),identifier(none,t)))),equal(none,identifier(none,t),typeof(none,empty_set(none),pow_subset(none,identifier(none,'OBJECT')))))))),forall(rodinpos('FCTX01',thm2,internal_element2T),[identifier(none,f),identifier(none,g),identifier(none,c),identifier(none,t),identifier(none,u),identifier(none,'M'),identifier(none,'N')],implication(none,conjunct(none,member(none,identifier(none,f),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),identifier(none,'OBJECT')))),conjunct(none,member(none,identifier(none,g),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),identifier(none,'OBJECT')))),conjunct(none,member(none,identifier(none,c),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),identifier(none,'OBJECT')))),conjunct(none,member(none,identifier(none,t),identifier(none,'OBJECT')),conjunct(none,member(none,identifier(none,u),identifier(none,'OBJECT')),conjunct(none,member(none,identifier(none,'M'),pow_subset(none,identifier(none,'OBJECT'))),conjunct(none,member(none,identifier(none,'N'),pow_subset(none,identifier(none,'OBJECT'))),conjunct(none,subset(none,identifier(none,'N'),identifier(none,'OBJECT')),conjunct(none,subset(none,identifier(none,'M'),identifier(none,'OBJECT')),conjunct(none,equal(none,intersection(none,identifier(none,'N'),identifier(none,'M')),typeof(none,empty_set(none),pow_subset(none,identifier(none,'OBJECT')))),conjunct(none,member(none,identifier(none,t),identifier(none,'M')),conjunct(none,member(none,identifier(none,f),total_function(none,set_subtraction(none,identifier(none,'M'),set_extension(none,[identifier(none,t)])),identifier(none,'M'))),conjunct(none,member(none,identifier(none,u),identifier(none,'N')),conjunct(none,member(none,identifier(none,c),total_bijection(none,identifier(none,'M'),identifier(none,'N'))),conjunct(none,equal(none,identifier(none,u),function(none,identifier(none,c),[identifier(none,t)])),equal(none,identifier(none,g),composition(none,reverse(none,identifier(none,c)),composition(none,identifier(none,f),identifier(none,c))))))))))))))))))),member(none,identifier(none,g),total_function(none,set_subtraction(none,identifier(none,'N'),set_extension(none,[identifier(none,u)])),identifier(none,'N'))))),forall(rodinpos('FCTX01',thm3,internal_element3T),[identifier(none,f),identifier(none,c),identifier(none,g),identifier(none,t),identifier(none,u),identifier(none,'M'),identifier(none,'N')],implication(none,conjunct(none,member(none,identifier(none,f),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),identifier(none,'OBJECT')))),conjunct(none,member(none,identifier(none,c),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),identifier(none,'OBJECT')))),conjunct(none,member(none,identifier(none,g),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),identifier(none,'OBJECT')))),conjunct(none,member(none,identifier(none,t),identifier(none,'OBJECT')),conjunct(none,member(none,identifier(none,u),identifier(none,'OBJECT')),conjunct(none,member(none,identifier(none,'M'),pow_subset(none,identifier(none,'OBJECT'))),conjunct(none,member(none,identifier(none,'N'),pow_subset(none,identifier(none,'OBJECT'))),conjunct(none,subset(none,identifier(none,'N'),identifier(none,'OBJECT')),conjunct(none,subset(none,identifier(none,'M'),identifier(none,'OBJECT')),conjunct(none,member(none,identifier(none,t),identifier(none,'M')),conjunct(none,member(none,identifier(none,f),total_function(none,set_subtraction(none,identifier(none,'M'),set_extension(none,[identifier(none,t)])),identifier(none,'M'))),conjunct(none,forall(none,[identifier(none,s)],implication(none,conjunct(none,member(none,identifier(none,s),pow_subset(none,identifier(none,'OBJECT'))),subset(none,identifier(none,s),image(none,reverse(none,identifier(none,f)),identifier(none,s)))),equal(none,identifier(none,s),typeof(none,empty_set(none),pow_subset(none,identifier(none,'OBJECT')))))),conjunct(none,member(none,identifier(none,u),identifier(none,'N')),conjunct(none,member(none,identifier(none,c),total_bijection(none,identifier(none,'M'),identifier(none,'N'))),conjunct(none,equal(none,identifier(none,u),function(none,identifier(none,c),[identifier(none,t)])),conjunct(none,equal(none,identifier(none,g),composition(none,reverse(none,identifier(none,c)),composition(none,identifier(none,f),identifier(none,c)))),member(none,identifier(none,g),total_function(none,set_subtraction(none,identifier(none,'N'),set_extension(none,[identifier(none,u)])),identifier(none,'N'))))))))))))))))))),forall(none,[identifier(none,w)],implication(none,conjunct(none,member(none,identifier(none,w),pow_subset(none,identifier(none,'OBJECT'))),subset(none,identifier(none,w),image(none,reverse(none,identifier(none,g)),identifier(none,w)))),equal(none,identifier(none,w),typeof(none,empty_set(none),pow_subset(none,identifier(none,'OBJECT')))))))),forall(rodinpos('FCTX01',thm4,internal_element4T),[identifier(none,f),identifier(none,g),identifier(none,t),identifier(none,u),identifier(none,x),identifier(none,'M'),identifier(none,'N')],implication(none,conjunct(none,member(none,identifier(none,f),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),identifier(none,'OBJECT')))),conjunct(none,member(none,identifier(none,g),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),identifier(none,'OBJECT')))),conjunct(none,member(none,identifier(none,t),identifier(none,'OBJECT')),conjunct(none,member(none,identifier(none,u),identifier(none,'OBJECT')),conjunct(none,member(none,identifier(none,x),identifier(none,'OBJECT')),conjunct(none,member(none,identifier(none,'M'),pow_subset(none,identifier(none,'OBJECT'))),conjunct(none,member(none,identifier(none,'N'),pow_subset(none,identifier(none,'OBJECT'))),conjunct(none,subset(none,identifier(none,'N'),identifier(none,'OBJECT')),conjunct(none,subset(none,identifier(none,'M'),identifier(none,'OBJECT')),conjunct(none,equal(none,intersection(none,identifier(none,'N'),identifier(none,'M')),typeof(none,empty_set(none),pow_subset(none,identifier(none,'OBJECT')))),conjunct(none,member(none,identifier(none,t),identifier(none,'M')),conjunct(none,member(none,identifier(none,f),total_function(none,set_subtraction(none,identifier(none,'M'),set_extension(none,[identifier(none,t)])),identifier(none,'M'))),conjunct(none,member(none,identifier(none,u),identifier(none,'N')),conjunct(none,member(none,identifier(none,g),total_function(none,set_subtraction(none,identifier(none,'N'),set_extension(none,[identifier(none,u)])),identifier(none,'N'))),member(none,identifier(none,x),identifier(none,'M')))))))))))))))),member(none,union(none,identifier(none,f),union(none,identifier(none,g),set_extension(none,[couple(none,[identifier(none,u),identifier(none,x)])]))),total_function(none,set_subtraction(none,union(none,identifier(none,'M'),identifier(none,'N')),set_extension(none,[identifier(none,t)])),union(none,identifier(none,'M'),identifier(none,'N')))))),forall(rodinpos('FCTX01',thm5,internal_element5T),[identifier(none,f),identifier(none,g),identifier(none,t),identifier(none,u),identifier(none,x),identifier(none,'M'),identifier(none,'N')],implication(none,conjunct(none,member(none,identifier(none,f),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),identifier(none,'OBJECT')))),conjunct(none,member(none,identifier(none,g),pow_subset(none,cartesian_product(none,identifier(none,'OBJECT'),identifier(none,'OBJECT')))),conjunct(none,member(none,identifier(none,t),identifier(none,'OBJECT')),conjunct(none,member(none,identifier(none,u),identifier(none,'OBJECT')),conjunct(none,member(none,identifier(none,x),identifier(none,'OBJECT')),conjunct(none,member(none,identifier(none,'M'),pow_subset(none,identifier(none,'OBJECT'))),conjunct(none,member(none,identifier(none,'N'),pow_subset(none,identifier(none,'OBJECT'))),conjunct(none,subset(none,identifier(none,'N'),identifier(none,'OBJECT')),conjunct(none,subset(none,identifier(none,'M'),identifier(none,'OBJECT')),conjunct(none,equal(none,intersection(none,identifier(none,'N'),identifier(none,'M')),typeof(none,empty_set(none),pow_subset(none,identifier(none,'OBJECT')))),conjunct(none,member(none,identifier(none,t),identifier(none,'M')),conjunct(none,member(none,identifier(none,f),total_function(none,set_subtraction(none,identifier(none,'M'),set_extension(none,[identifier(none,t)])),identifier(none,'M'))),conjunct(none,member(none,identifier(none,u),identifier(none,'N')),conjunct(none,member(none,identifier(none,g),total_function(none,set_subtraction(none,identifier(none,'N'),set_extension(none,[identifier(none,u)])),identifier(none,'N'))),conjunct(none,member(none,identifier(none,x),identifier(none,'M')),conjunct(none,forall(none,[identifier(none,'A')],implication(none,conjunct(none,member(none,identifier(none,'A'),pow_subset(none,identifier(none,'OBJECT'))),subset(none,identifier(none,'A'),image(none,reverse(none,identifier(none,f)),identifier(none,'A')))),equal(none,identifier(none,'A'),typeof(none,empty_set(none),pow_subset(none,identifier(none,'OBJECT')))))),conjunct(none,forall(none,[identifier(none,'B')],implication(none,conjunct(none,member(none,identifier(none,'B'),pow_subset(none,identifier(none,'OBJECT'))),subset(none,identifier(none,'B'),image(none,reverse(none,identifier(none,g)),identifier(none,'B')))),equal(none,identifier(none,'B'),typeof(none,empty_set(none),pow_subset(none,identifier(none,'OBJECT')))))),member(none,union(none,identifier(none,f),union(none,identifier(none,g),set_extension(none,[couple(none,[identifier(none,u),identifier(none,x)])]))),total_function(none,set_subtraction(none,union(none,identifier(none,'M'),identifier(none,'N')),set_extension(none,[identifier(none,t)])),union(none,identifier(none,'M'),identifier(none,'N'))))))))))))))))))))),forall(none,[identifier(none,'C')],implication(none,conjunct(none,member(none,identifier(none,'C'),pow_subset(none,identifier(none,'OBJECT'))),subset(none,identifier(none,'C'),image(none,reverse(none,union(none,identifier(none,f),union(none,identifier(none,g),set_extension(none,[couple(none,[identifier(none,u),identifier(none,x)])])))),identifier(none,'C')))),equal(none,identifier(none,'C'),typeof(none,empty_set(none),pow_subset(none,identifier(none,'OBJECT'))))))))]),sets(none,[])]),event_b_context(none,'FCTX02',[extends(none,[]),constants(none,[identifier(none,'CONTENT'),identifier(none,rname)]),abstract_constants(none,[]),axioms(none,[equal(rodinpos('FCTX02',axm1,internal_axm1A),identifier(none,'CONTENT'),partial_function(none,natural_set(none),identifier(none,'DATA'))),member(rodinpos('FCTX02',axm2,internal_axm2A),typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'DATA')))),identifier(none,'CONTENT')),member(rodinpos('FCTX02',axm3,internal_axm3A),identifier(none,rname),identifier(none,'NAME'))]),theorems(none,[]),sets(none,[deferred_set(none,'DATA'),deferred_set(none,'NAME')])])],[exporter_version(3),po('FCTX','Well-definedness of Axiom',[axiom(axm5)],true),po('FCTX','Well-definedness of Axiom',[axiom(axm6)],true),po('FCTX','Well-definedness of Axiom',[axiom(axm7)],true),po('FCTX','Theorem',[axiom(thm5)],true),po('FCTX','Well-definedness of Theorem',[axiom(thm1)],true),po('FCTX','Theorem',[axiom(thm1)],true),po('FCTX','Well-definedness of Theorem',[axiom(thm2)],true),po('FCTX','Theorem',[axiom(thm2)],true),po('FCTX','Well-definedness of Theorem',[axiom(thm3)],true),po('FCTX','Theorem',[axiom(thm3)],true),po('FCTX01','Theorem',[axiom(thm1)],true),po('FCTX01','Well-definedness of Theorem',[axiom(thm2)],true),po('FCTX01','Theorem',[axiom(thm2)],true),po('FCTX01','Well-definedness of Theorem',[axiom(thm3)],true),po('FCTX01','Theorem',[axiom(thm3)],true),po('FCTX01','Theorem',[axiom(thm4)],true),po('FCTX01','Theorem',[axiom(thm5)],true),po('FMCH02','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1)],true),po('FMCH02','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv2)],true),po('FMCH02','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3)],true),po('FMCH02','Invariant preservation',[event(crt_file),event(crt_file),invariant(inv1)],true),po('FMCH02','Invariant preservation',[event(crt_file),event(crt_file),invariant(inv2)],true),po('FMCH02','Invariant preservation',[event(delete),event(delete),invariant(inv1)],true),po('FMCH02','Invariant preservation',[event(delete),event(delete),invariant(inv2)],true),po('FMCH02','Invariant preservation',[event(copy),event(copy),invariant(inv1)],true),po('FMCH02','Invariant preservation',[event(copy),event(copy),invariant(inv2)],true),po('FMCH02','Invariant preservation',[event(readfile),invariant(inv3)],true),po('FMCH02','Well-definedness of action',[action(act1)],true),po('FMCH02','Invariant preservation',[event(writefile),invariant(inv1)],true),po('FMCH02','Well-definedness of action',[action(act1)],true),po('FMCH02','Invariant preservation',[event(open),invariant(inv2)],true),po('FMCH02','Invariant preservation',[event(open),invariant(inv3)],true),po('FMCH02','Invariant preservation',[event(close),invariant(inv2)],true),po('FMCH02','Invariant preservation',[event(close),invariant(inv3)],true),po('FMCH01','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv2)],true),po('FMCH01','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3)],true),po('FMCH01','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv4)],true),po('FMCH01','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv5)],true),po('FMCH01','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv6)],true),po('FMCH01','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1)],true),po('FMCH01','Action simulation',[event('INITIALISATION'),action(act4),event('INITIALISATION')],true),po('FMCH01','Invariant preservation',[event(newobj),event(mkdir),invariant(inv2)],true),po('FMCH01','Invariant preservation',[event(newobj),event(mkdir),invariant(inv3)],true),po('FMCH01','Invariant preservation',[event(newobj),event(mkdir),invariant(inv4)],true),po('FMCH01','Invariant preservation',[event(newobj),event(mkdir),invariant(inv5)],true),po('FMCH01','Invariant preservation',[event(newobj),event(mkdir),invariant(inv6)],true),po('FMCH01','Invariant preservation',[event(newobj),event(mkdir),invariant(inv1)],true),po('FMCH01','Guard strengthening (split)',[event(newobj),guard(grd1),event(newobj),event(mkdir)],true),po('FMCH01','Guard strengthening (split)',[event(newobj),guard(grd2),event(newobj),event(mkdir)],true),po('FMCH01','Action simulation',[event(newobj),action(act3),event(mkdir)],true),po('FMCH01','Invariant preservation',[event(newobj),event(crt_file),invariant(inv2)],true),po('FMCH01','Invariant preservation',[event(newobj),event(crt_file),invariant(inv3)],true),po('FMCH01','Invariant preservation',[event(newobj),event(crt_file),invariant(inv4)],true),po('FMCH01','Invariant preservation',[event(newobj),event(crt_file),invariant(inv5)],true),po('FMCH01','Invariant preservation',[event(newobj),event(crt_file),invariant(inv1)],true),po('FMCH01','Guard strengthening (split)',[event(newobj),guard(grd1),event(newobj),event(crt_file)],true),po('FMCH01','Guard strengthening (split)',[event(newobj),guard(grd2),event(newobj),event(crt_file)],true),po('FMCH01','Action simulation',[event(newobj),action(act3),event(crt_file)],true),po('FMCH01','Well-definedness of Guard',[guard(grd6),event(move)],true),po('FMCH01','Invariant preservation',[event(move),event(move),invariant(inv1)],true),po('FMCH01','Guard strengthening (split)',[event(move),guard(grd1),event(move),event(move)],true),po('FMCH01','Guard strengthening (split)',[event(move),guard(grd3),event(move),event(move)],true),po('FMCH01','Well-definedness of Guard',[guard(grd6),event(delete)],true),po('FMCH01','Invariant preservation',[event(delete),event(delete),invariant(inv2)],true),po('FMCH01','Invariant preservation',[event(delete),event(delete),invariant(inv3)],true),po('FMCH01','Invariant preservation',[event(delete),event(delete),invariant(inv4)],true),po('FMCH01','Invariant preservation',[event(delete),event(delete),invariant(inv5)],true),po('FMCH01','Invariant preservation',[event(delete),event(delete),invariant(inv6)],true),po('FMCH01','Invariant preservation',[event(delete),event(delete),invariant(inv1)],true),po('FMCH01','Guard strengthening (split)',[event(delete),guard(grd1),event(delete),event(delete)],true),po('FMCH01','Guard strengthening (split)',[event(delete),guard(grd4),event(delete),event(delete)],true),po('FMCH01','Action simulation',[event(delete),action(act4),event(delete)],true),po('FMCH01','Well-definedness of Guard',[guard(grd7),event(copy)],true),po('FMCH01','Well-definedness of Guard',[guard(grd2),event(copy)],true),po('FMCH01','Invariant preservation',[event(copy),event(copy),invariant(inv2)],true),po('FMCH01','Invariant preservation',[event(copy),event(copy),invariant(inv3)],true),po('FMCH01','Invariant preservation',[event(copy),event(copy),invariant(inv4)],true),po('FMCH01','Invariant preservation',[event(copy),event(copy),invariant(inv5)],true),po('FMCH01','Invariant preservation',[event(copy),event(copy),invariant(inv6)],true),po('FMCH01','Invariant preservation',[event(copy),event(copy),invariant(inv1)],true),po('FMCH01','Guard strengthening (split)',[event(copy),guard(grd1),event(copy),event(copy)],true),po('FMCH01','Guard strengthening (split)',[event(copy),guard(grd9),event(copy),event(copy)],true),po('FMCH01','Guard strengthening (split)',[event(copy),guard(grd3),event(copy),event(copy)],true),po('FMCH01','Guard strengthening (split)',[event(copy),guard(grd5),event(copy),event(copy)],true),po('FMCH00','Well-definedness of Theorem',[invariant(thm1)],true),po('FMCH00','Theorem',[invariant(thm1)],true),po('FMCH00','Theorem',[invariant(thm3)],true),po('FMCH00','Well-definedness of Theorem',[invariant(thm4)],true),po('FMCH00','Theorem',[invariant(thm4)],true),po('FMCH00','Well-definedness of Theorem',[invariant(thm2)],true),po('FMCH00','Theorem',[invariant(thm2)],true),po('FMCH00','Well-definedness of Theorem',[invariant(thm5)],true),po('FMCH00','Theorem',[invariant(thm5)],true),po('FMCH00','Well-definedness of Theorem',[invariant(thm6)],true),po('FMCH00','Theorem',[invariant(thm6)],true),po('FMCH00','Well-definedness of Theorem',[invariant(thm7)],true),po('FMCH00','Theorem',[invariant(thm7)],true),po('FMCH00','Well-definedness of Theorem',[invariant(thm8)],true),po('FMCH00','Theorem',[invariant(thm8)],true),po('FMCH00','Well-definedness of Theorem',[invariant(thm9)],true),po('FMCH00','Theorem',[invariant(thm9)],true),po('FMCH00','Invariant establishment',[event('INITIALISATION'),invariant(inv6)],true),po('FMCH00','Invariant establishment',[event('INITIALISATION'),invariant(inv8)],true),po('FMCH00','Invariant establishment',[event('INITIALISATION'),invariant(inv10)],true),po('FMCH00','Invariant preservation',[event(newobj),invariant(inv6)],true),po('FMCH00','Invariant preservation',[event(newobj),invariant(inv8)],true),po('FMCH00','Invariant preservation',[event(newobj),invariant(inv10)],true),po('FMCH00','Well-definedness of Guard',[guard(grd6),event(move)],true),po('FMCH00','Invariant preservation',[event(move),invariant(inv8)],true),po('FMCH00','Invariant preservation',[event(move),invariant(inv10)],true),po('FMCH00','Well-definedness of Guard',[guard(grd6),event(delete)],true),po('FMCH00','Invariant preservation',[event(delete),invariant(inv6)],true),po('FMCH00','Invariant preservation',[event(delete),invariant(inv8)],true),po('FMCH00','Invariant preservation',[event(delete),invariant(inv10)],true),po('FMCH00','Well-definedness of Guard',[guard(grd7),event(copy)],true),po('FMCH00','Well-definedness of Guard',[guard(grd2),event(copy)],true),po('FMCH00','Invariant preservation',[event(copy),invariant(inv6)],true),po('FMCH00','Invariant preservation',[event(copy),invariant(inv8)],true),po('FMCH00','Invariant preservation',[event(copy),invariant(inv10)],true)],_Error)).
2