1		package(load_event_b_project([],[event_b_context(none,'MySequences',[extends(none,[]),constants(none,[identifier(none,first),identifier(none,front),identifier(none,last),identifier(none,seq),identifier(none,seq1),identifier(none,size),identifier(none,t1),identifier(none,t2),identifier(none,tail)]),abstract_constants(none,[]),axioms(none,[conjunct(rodinpos('MySequences',axm0,'_fm2SQr0zEeWoZ5noOctNXg'),member(none,identifier(none,t1),identifier(none,'T')),conjunct(none,member(none,identifier(none,t2),identifier(none,'T')),not_equal(none,identifier(none,t1),identifier(none,t2)))),equal(rodinpos('MySequences',axm1,'_zmyLcb0zEeWoZ5noOctNXg'),identifier(none,seq),event_b_comprehension_set(none,[identifier(none,f)],identifier(none,f),conjunct(none,member(none,identifier(none,f),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'T')))),conjunct(none,member(none,identifier(none,f),partial_function(none,integer_set(none),identifier(none,'T'))),exists(none,[identifier(none,n)],conjunct(none,member(none,identifier(none,n),integer_set(none)),conjunct(none,greater_equal(none,identifier(none,n),integer(none,0)),member(none,identifier(none,f),total_function(none,interval(none,integer(none,1),identifier(none,n)),identifier(none,'T')))))))))),equal(rodinpos('MySequences',axm2,'_zmyLcr0zEeWoZ5noOctNXg'),identifier(none,seq1),set_subtraction(none,identifier(none,seq),set_extension(none,[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'T'))))]))),equal(rodinpos('MySequences',axm3,'_zmyLc70zEeWoZ5noOctNXg'),identifier(none,size),event_b_comprehension_set(none,[identifier(none,s)],couple(none,[identifier(none,s),card(none,identifier(none,s))]),conjunct(none,member(none,identifier(none,s),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'T')))),member(none,identifier(none,s),identifier(none,seq))))),equal(rodinpos('MySequences',axm4,'_zmyLdL0zEeWoZ5noOctNXg'),identifier(none,first),event_b_comprehension_set(none,[identifier(none,s)],couple(none,[identifier(none,s),function(none,identifier(none,s),[integer(none,1)])]),conjunct(none,member(none,identifier(none,s),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'T')))),member(none,identifier(none,s),identifier(none,seq1))))),equal(rodinpos('MySequences',axm5,'_zmyygL0zEeWoZ5noOctNXg'),identifier(none,last),event_b_comprehension_set(none,[identifier(none,s)],couple(none,[identifier(none,s),function(none,identifier(none,s),[function(none,identifier(none,size),[identifier(none,s)])])]),conjunct(none,member(none,identifier(none,s),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'T')))),member(none,identifier(none,s),identifier(none,seq1))))),equal(rodinpos('MySequences',axm6,'_zmyygb0zEeWoZ5noOctNXg'),identifier(none,tail),event_b_comprehension_set(none,[identifier(none,s)],couple(none,[identifier(none,s),composition(none,successor(none),domain_subtraction(none,set_extension(none,[integer(none,1)]),identifier(none,s)))]),conjunct(none,member(none,identifier(none,s),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'T')))),member(none,identifier(none,s),identifier(none,seq))))),equal(rodinpos('MySequences',axm7,'_6_Enob0zEeWoZ5noOctNXg'),identifier(none,front),event_b_comprehension_set(none,[identifier(none,s)],couple(none,[identifier(none,s),domain_subtraction(none,set_extension(none,[function(none,identifier(none,size),[identifier(none,s)])]),identifier(none,s))]),conjunct(none,member(none,identifier(none,s),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'T')))),member(none,identifier(none,s),identifier(none,seq)))))]),theorems(none,[member(rodinpos('MySequences',thm0,'_6_Enor0zEeWoZ5noOctNXg'),typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'T')))),identifier(none,seq)),member(rodinpos('MySequences',thm1,'_9GWdML0zEeWoZ5noOctNXg'),set_extension(none,[couple(none,[integer(none,1),identifier(none,t1)])]),identifier(none,seq)),member(rodinpos('MySequences',thm2,'_9GWdMb0zEeWoZ5noOctNXg'),set_extension(none,[couple(none,[integer(none,1),identifier(none,t1)]),couple(none,[integer(none,2),identifier(none,t2)])]),identifier(none,seq)),not_member(rodinpos('MySequences',thm3,'_Ks2vIb00EeWoZ5noOctNXg'),set_extension(none,[couple(none,[integer(none,1),identifier(none,t1)]),couple(none,[integer(none,1),identifier(none,t2)])]),identifier(none,seq)),not_member(rodinpos('MySequences',thm4,'_Q7ro4L00EeWoZ5noOctNXg'),set_extension(none,[couple(none,[integer(none,0),identifier(none,t1)])]),identifier(none,seq)),not_member(rodinpos('MySequences',thm5,'_fbKKMr00EeWoZ5noOctNXg'),set_extension(none,[couple(none,[integer(none,1),identifier(none,t1)]),couple(none,[integer(none,3),identifier(none,t2)])]),identifier(none,seq)),not_member(rodinpos('MySequences',thm6,'_fbKKM700EeWoZ5noOctNXg'),typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'T')))),identifier(none,seq1)),member(rodinpos('MySequences',thm7,'_fbKKNL00EeWoZ5noOctNXg'),set_extension(none,[couple(none,[integer(none,1),identifier(none,t1)])]),identifier(none,seq1)),conjunct(rodinpos('MySequences',thm8,'_fbKxQL00EeWoZ5noOctNXg'),equal(none,function(none,identifier(none,size),[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,integer_set(none),identifier(none,'T'))))]),integer(none,0)),equal(none,function(none,identifier(none,size),[set_extension(none,[couple(none,[integer(none,1),identifier(none,t1)])])]),integer(none,1))),conjunct(rodinpos('MySequences',thm9,'_fbKxQb00EeWoZ5noOctNXg'),equal(none,function(none,identifier(none,first),[set_extension(none,[couple(none,[integer(none,1),identifier(none,t1)])])]),identifier(none,t1)),equal(none,function(none,identifier(none,last),[set_extension(none,[couple(none,[integer(none,1),identifier(none,t1)])])]),identifier(none,t1))),equal(rodinpos('MySequences',thm10,'_JxmLUr01EeWoZ5noOctNXg'),function(none,identifier(none,first),[set_extension(none,[couple(none,[integer(none,1),identifier(none,t1)]),couple(none,[integer(none,2),identifier(none,t2)])])]),identifier(none,t1)),equal(rodinpos('MySequences',thm11,'_JxmLU701EeWoZ5noOctNXg'),function(none,identifier(none,last),[set_extension(none,[couple(none,[integer(none,1),identifier(none,t1)]),couple(none,[integer(none,2),identifier(none,t2)])])]),identifier(none,t2)),equal(rodinpos('MySequences',thm12,'_dP_dsL01EeWoZ5noOctNXg'),function(none,identifier(none,tail),[set_extension(none,[couple(none,[integer(none,1),identifier(none,t1)]),couple(none,[integer(none,2),identifier(none,t2)])])]),set_extension(none,[couple(none,[integer(none,1),identifier(none,t2)])])),equal(rodinpos('MySequences',thm13,'_dP_dsb01EeWoZ5noOctNXg'),function(none,identifier(none,front),[set_extension(none,[couple(none,[integer(none,1),identifier(none,t1)]),couple(none,[integer(none,2),identifier(none,t2)])])]),set_extension(none,[couple(none,[integer(none,1),identifier(none,t1)])]))]),sets(none,[deferred_set(none,'T')])])],[exporter_version(3),po('MySequences','Well-definedness of Axiom',[axiom(axm3)],false),po('MySequences','Well-definedness of Axiom',[axiom(axm4)],true),po('MySequences','Well-definedness of Axiom',[axiom(axm5)],true),po('MySequences','Well-definedness of Axiom',[axiom(axm7)],true),po('MySequences','Theorem',[axiom(thm0)],true),po('MySequences','Theorem',[axiom(thm1)],true),po('MySequences','Theorem',[axiom(thm2)],true),po('MySequences','Theorem',[axiom(thm3)],true),po('MySequences','Theorem',[axiom(thm4)],true),po('MySequences','Theorem',[axiom(thm5)],false),po('MySequences','Theorem',[axiom(thm6)],true),po('MySequences','Theorem',[axiom(thm7)],true),po('MySequences','Well-definedness of Theorem',[axiom(thm8)],true),po('MySequences','Theorem',[axiom(thm8)],true),po('MySequences','Well-definedness of Theorem',[axiom(thm9)],true),po('MySequences','Theorem',[axiom(thm9)],true),po('MySequences','Well-definedness of Theorem',[axiom(thm10)],true),po('MySequences','Theorem',[axiom(thm10)],true),po('MySequences','Well-definedness of Theorem',[axiom(thm11)],true),po('MySequences','Theorem',[axiom(thm11)],true),po('MySequences','Well-definedness of Theorem',[axiom(thm12)],true),po('MySequences','Theorem',[axiom(thm12)],true),po('MySequences','Well-definedness of Theorem',[axiom(thm13)],true),po('MySequences','Theorem',[axiom(thm13)],false)],_Error)).
2