1		package(load_event_b_project([event_b_model(none,'ListLawsMC_inf',[sees(none,[]),variables(none,[identifier(none,'SS'),identifier(none,'TT'),identifier(none,'VV'),identifier(none,setX)]),invariant(none,[member(rodinpos('ListLawsMC_inf',inv1,')'),identifier(none,setX),pow_subset(none,typeof(none,extended_expr(none,'List',[integer_set(none)],[]),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[]))))),conjunct(rodinpos('ListLawsMC_inf',inv2,'+'),member(none,identifier(none,'SS'),pow_subset(none,identifier(none,setX))),member(none,identifier(none,'TT'),pow_subset(none,identifier(none,setX)))),member(rodinpos('ListLawsMC_inf',inv3,'-'),identifier(none,'VV'),pow_subset(none,identifier(none,setX))),conjunct(rodinpos('ListLawsMC_inf',inv4,'1'),equal(none,union(none,identifier(none,'SS'),identifier(none,'SS')),identifier(none,'SS')),conjunct(none,equal(none,identifier(none,'SS'),union(none,identifier(none,'SS'),typeof(none,empty_set(none),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[]))))),conjunct(none,equal(none,identifier(none,'SS'),intersection(none,identifier(none,'SS'),identifier(none,'SS'))),equal(none,identifier(none,'SS'),set_subtraction(none,identifier(none,'SS'),typeof(none,empty_set(none),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[])))))))),conjunct(rodinpos('ListLawsMC_inf',inv5,'2'),equal(none,intersection(none,identifier(none,'SS'),typeof(none,empty_set(none),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[])))),typeof(none,empty_set(none),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[])))),conjunct(none,equal(none,typeof(none,empty_set(none),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[]))),set_subtraction(none,identifier(none,'SS'),identifier(none,'SS'))),equal(none,set_subtraction(none,typeof(none,empty_set(none),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[]))),identifier(none,'SS')),typeof(none,empty_set(none),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[])))))),conjunct(rodinpos('ListLawsMC_inf',inv6,'3'),equal(none,union(none,identifier(none,'SS'),identifier(none,'TT')),union(none,identifier(none,'TT'),identifier(none,'SS'))),equal(none,intersection(none,identifier(none,'SS'),identifier(none,'TT')),intersection(none,identifier(none,'TT'),identifier(none,'SS')))),conjunct(rodinpos('ListLawsMC_inf',inv7,'4'),equal(none,union(none,identifier(none,'SS'),union(none,identifier(none,'TT'),identifier(none,'VV'))),union(none,union(none,identifier(none,'SS'),identifier(none,'TT')),identifier(none,'VV'))),equal(none,intersection(none,identifier(none,'SS'),intersection(none,identifier(none,'TT'),identifier(none,'VV'))),intersection(none,intersection(none,identifier(none,'SS'),identifier(none,'TT')),identifier(none,'VV')))),equal(rodinpos('ListLawsMC_inf',inv8,'5'),union(none,identifier(none,'SS'),intersection(none,identifier(none,'TT'),identifier(none,'VV'))),intersection(none,union(none,identifier(none,'SS'),identifier(none,'TT')),union(none,identifier(none,'SS'),identifier(none,'VV')))),equal(rodinpos('ListLawsMC_inf',inv9,'6'),intersection(none,identifier(none,'SS'),union(none,identifier(none,'TT'),identifier(none,'VV'))),union(none,intersection(none,identifier(none,'SS'),identifier(none,'TT')),intersection(none,identifier(none,'SS'),identifier(none,'VV')))),equal(rodinpos('ListLawsMC_inf',inv10,'7'),union(none,intersection(none,identifier(none,'SS'),identifier(none,'TT')),set_subtraction(none,identifier(none,'SS'),identifier(none,'TT'))),identifier(none,'SS')),equal(rodinpos('ListLawsMC_inf',inv11,'8'),intersection(none,set_subtraction(none,identifier(none,'SS'),identifier(none,'TT')),identifier(none,'TT')),typeof(none,empty_set(none),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[])))),equal(rodinpos('ListLawsMC_inf',inv12,'9'),set_subtraction(none,identifier(none,'SS'),set_subtraction(none,identifier(none,'TT'),identifier(none,'VV'))),union(none,set_subtraction(none,identifier(none,'SS'),identifier(none,'TT')),intersection(none,identifier(none,'SS'),identifier(none,'VV')))),equal(rodinpos('ListLawsMC_inf',inv13,':'),set_subtraction(none,set_subtraction(none,identifier(none,'SS'),identifier(none,'TT')),identifier(none,'VV')),set_subtraction(none,identifier(none,'SS'),union(none,identifier(none,'TT'),identifier(none,'VV')))),equal(rodinpos('ListLawsMC_inf',inv14,';'),union(none,identifier(none,'SS'),set_subtraction(none,identifier(none,'TT'),identifier(none,'VV'))),set_subtraction(none,union(none,identifier(none,'SS'),identifier(none,'TT')),set_subtraction(none,identifier(none,'VV'),identifier(none,'SS')))),equal(rodinpos('ListLawsMC_inf',inv15,'='),intersection(none,identifier(none,'SS'),set_subtraction(none,identifier(none,'TT'),identifier(none,'VV'))),set_subtraction(none,intersection(none,identifier(none,'SS'),identifier(none,'TT')),identifier(none,'VV'))),equal(rodinpos('ListLawsMC_inf',inv16,'>'),set_subtraction(none,union(none,identifier(none,'SS'),identifier(none,'TT')),identifier(none,'VV')),union(none,set_subtraction(none,identifier(none,'SS'),identifier(none,'VV')),set_subtraction(none,identifier(none,'TT'),identifier(none,'VV')))),equal(rodinpos('ListLawsMC_inf',inv17,'?'),set_subtraction(none,identifier(none,'SS'),intersection(none,identifier(none,'TT'),identifier(none,'VV'))),union(none,set_subtraction(none,identifier(none,'SS'),identifier(none,'TT')),set_subtraction(none,identifier(none,'SS'),identifier(none,'VV')))),conjunct(rodinpos('ListLawsMC_inf',inv18,'@'),subset(none,identifier(none,'SS'),union(none,identifier(none,'SS'),identifier(none,'TT'))),subset(none,identifier(none,'TT'),union(none,identifier(none,'SS'),identifier(none,'TT')))),implication(rodinpos('ListLawsMC_inf',inv19,'A'),conjunct(none,subset(none,identifier(none,'SS'),identifier(none,'VV')),subset(none,identifier(none,'TT'),identifier(none,'VV'))),subset(none,union(none,identifier(none,'SS'),identifier(none,'TT')),identifier(none,'VV'))),conjunct(rodinpos('ListLawsMC_inf',inv20,'B'),subset(none,intersection(none,identifier(none,'SS'),identifier(none,'TT')),identifier(none,'SS')),subset(none,intersection(none,identifier(none,'SS'),identifier(none,'TT')),identifier(none,'TT'))),implication(rodinpos('ListLawsMC_inf',inv21,'C'),conjunct(none,subset(none,identifier(none,'VV'),identifier(none,'SS')),subset(none,identifier(none,'VV'),identifier(none,'TT'))),subset(none,identifier(none,'VV'),intersection(none,identifier(none,'SS'),identifier(none,'TT')))),equal(rodinpos('ListLawsMC_inf',inv22,'D'),event_b_comprehension_set(none,[identifier(none,xx)],identifier(none,xx),conjunct(none,member(none,identifier(none,xx),extended_expr(none,'List',[integer_set(none)],[])),conjunct(none,member(none,identifier(none,xx),identifier(none,'SS')),member(none,identifier(none,xx),identifier(none,'TT'))))),intersection(none,identifier(none,'SS'),identifier(none,'TT'))),equal(rodinpos('ListLawsMC_inf',inv23,'E'),event_b_comprehension_set(none,[identifier(none,xx)],identifier(none,xx),conjunct(none,member(none,identifier(none,xx),extended_expr(none,'List',[integer_set(none)],[])),conjunct(none,member(none,identifier(none,xx),identifier(none,setX)),disjunct(none,member(none,identifier(none,xx),identifier(none,'SS')),member(none,identifier(none,xx),identifier(none,'TT')))))),union(none,identifier(none,'SS'),identifier(none,'TT'))),equal(rodinpos('ListLawsMC_inf',inv24,'F'),event_b_comprehension_set(none,[identifier(none,xx)],identifier(none,xx),conjunct(none,member(none,identifier(none,xx),extended_expr(none,'List',[integer_set(none)],[])),conjunct(none,member(none,identifier(none,xx),identifier(none,setX)),conjunct(none,member(none,identifier(none,xx),identifier(none,'SS')),disjunct(none,member(none,identifier(none,xx),identifier(none,'TT')),member(none,identifier(none,xx),identifier(none,'VV'))))))),intersection(none,identifier(none,'SS'),union(none,identifier(none,'VV'),identifier(none,'TT')))),equal(rodinpos('ListLawsMC_inf',inv25,'G'),event_b_comprehension_set(none,[identifier(none,xx)],identifier(none,xx),conjunct(none,member(none,identifier(none,xx),extended_expr(none,'List',[integer_set(none)],[])),conjunct(none,member(none,identifier(none,xx),identifier(none,'SS')),negation(none,member(none,identifier(none,xx),identifier(none,'TT')))))),set_subtraction(none,identifier(none,'SS'),identifier(none,'TT'))),forall(rodinpos('ListLawsMC_inf',inv26,'H'),[identifier(none,xx)],implication(none,conjunct(none,member(none,identifier(none,xx),extended_expr(none,'List',[integer_set(none)],[])),conjunct(none,member(none,identifier(none,xx),identifier(none,'SS')),member(none,identifier(none,xx),identifier(none,'TT')))),member(none,identifier(none,xx),intersection(none,identifier(none,'SS'),identifier(none,'TT'))))),forall(rodinpos('ListLawsMC_inf',inv27,'I'),[identifier(none,xx)],implication(none,conjunct(none,member(none,identifier(none,xx),extended_expr(none,'List',[integer_set(none)],[])),conjunct(none,member(none,identifier(none,xx),identifier(none,'SS')),negation(none,member(none,identifier(none,xx),identifier(none,'TT'))))),conjunct(none,member(none,identifier(none,xx),set_subtraction(none,identifier(none,'SS'),identifier(none,'TT'))),not_member(none,identifier(none,xx),identifier(none,'TT'))))),implication(rodinpos('ListLawsMC_inf',inv28,'J'),exists(none,[identifier(none,xx)],conjunct(none,member(none,identifier(none,xx),extended_expr(none,'List',[integer_set(none)],[])),conjunct(none,member(none,identifier(none,xx),identifier(none,'SS')),conjunct(none,member(none,identifier(none,xx),identifier(none,'TT')),member(none,identifier(none,xx),identifier(none,'VV')))))),negation(none,equal(none,intersection(none,identifier(none,'SS'),intersection(none,identifier(none,'TT'),identifier(none,'VV'))),typeof(none,empty_set(none),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[])))))),implication(rodinpos('ListLawsMC_inf',inv29,'K'),exists(none,[identifier(none,xx)],conjunct(none,member(none,identifier(none,xx),extended_expr(none,'List',[integer_set(none)],[])),conjunct(none,conjunct(none,member(none,identifier(none,xx),identifier(none,'SS')),not_member(none,identifier(none,xx),identifier(none,'TT'))),negation(none,equal(none,union(none,identifier(none,'SS'),identifier(none,'TT')),identifier(none,'TT')))))),negation(none,equal(none,set_subtraction(none,identifier(none,'SS'),identifier(none,'TT')),typeof(none,empty_set(none),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[])))))),disjunct(rodinpos('ListLawsMC_inf',inv30,'L'),subset_strict(none,identifier(none,'SS'),identifier(none,'VV')),not_subset_strict(none,identifier(none,'SS'),identifier(none,'VV'))),implication(rodinpos('ListLawsMC_inf',inv31,'N'),conjunct(none,subset_strict(none,identifier(none,'VV'),identifier(none,'SS')),subset(none,identifier(none,'SS'),identifier(none,'TT'))),subset_strict(none,identifier(none,'VV'),identifier(none,'TT'))),implication(rodinpos('ListLawsMC_inf',inv32,'O'),conjunct(none,subset(none,identifier(none,'VV'),identifier(none,'SS')),subset_strict(none,identifier(none,'SS'),identifier(none,'TT'))),subset_strict(none,identifier(none,'VV'),identifier(none,'TT'))),disjunct(rodinpos('ListLawsMC_inf',inv33,'P'),subset(none,identifier(none,'SS'),identifier(none,'VV')),not_subset(none,identifier(none,'SS'),identifier(none,'VV'))),disjunct(rodinpos('ListLawsMC_inf',inv34,'Q'),member(none,identifier(none,'SS'),pow_subset(none,identifier(none,'TT'))),not_member(none,identifier(none,'SS'),pow_subset(none,identifier(none,'TT')))),implication(rodinpos('ListLawsMC_inf',inv35,'R'),conjunct(none,subset(none,identifier(none,'SS'),identifier(none,'VV')),not_subset_strict(none,identifier(none,'SS'),identifier(none,'VV'))),equal(none,identifier(none,'SS'),identifier(none,'VV'))),implication(rodinpos('ListLawsMC_inf',inv36,'S'),subset(none,identifier(none,'SS'),identifier(none,'VV')),equivalence(none,not_equal(none,identifier(none,'SS'),identifier(none,'VV')),subset_strict(none,identifier(none,'SS'),identifier(none,'VV')))),implication(rodinpos('ListLawsMC_inf',inv37,'T'),subset_strict(none,identifier(none,'SS'),identifier(none,'VV')),not_equal(none,identifier(none,'SS'),identifier(none,'VV'))),implication(rodinpos('ListLawsMC_inf',inv38,'U'),equal(none,identifier(none,'SS'),identifier(none,'VV')),not_subset_strict(none,identifier(none,'SS'),identifier(none,'VV'))),implication(rodinpos('ListLawsMC_inf',inv39,'V'),subset_strict(none,identifier(none,'SS'),identifier(none,'VV')),subset(none,identifier(none,'SS'),identifier(none,'VV'))),implication(rodinpos('ListLawsMC_inf',inv40,'W'),subset_strict(none,identifier(none,'SS'),identifier(none,'VV')),exists(none,[identifier(none,xx)],conjunct(none,member(none,identifier(none,xx),extended_expr(none,'List',[integer_set(none)],[])),conjunct(none,member(none,identifier(none,xx),identifier(none,'VV')),not_member(none,identifier(none,xx),identifier(none,'SS')))))),equivalence(rodinpos('ListLawsMC_inf',inv41,'X'),subset(none,identifier(none,'SS'),identifier(none,'VV')),forall(none,[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),extended_expr(none,'List',[integer_set(none)],[])),member(none,identifier(none,x),identifier(none,'SS'))),member(none,identifier(none,x),identifier(none,'VV'))))),implication(rodinpos('ListLawsMC_inf',inv42,'Y'),subset_strict(none,identifier(none,'SS'),identifier(none,'VV')),less(none,card(none,identifier(none,'SS')),card(none,identifier(none,'VV')))),implication(rodinpos('ListLawsMC_inf',inv43,'Z'),subset(none,identifier(none,'SS'),identifier(none,'VV')),less_equal(none,card(none,identifier(none,'SS')),card(none,identifier(none,'VV')))),implication(rodinpos('ListLawsMC_inf',inv44,'['),less(none,card(none,identifier(none,'SS')),card(none,identifier(none,'VV'))),not_subset(none,identifier(none,'VV'),identifier(none,'SS'))),less_equal(rodinpos('ListLawsMC_inf',inv45,'\\'),card(none,union(none,identifier(none,'SS'),identifier(none,'VV'))),add(none,card(none,identifier(none,'SS')),card(none,identifier(none,'VV')))),implication(rodinpos('ListLawsMC_inf',inv46,']'),equal(none,card(none,identifier(none,'SS')),card(none,identifier(none,'VV'))),not_subset_strict(none,identifier(none,'VV'),identifier(none,'SS'))),implication(rodinpos('ListLawsMC_inf',inv47,'^'),less_equal(none,card(none,identifier(none,'SS')),card(none,identifier(none,'VV'))),not_subset_strict(none,identifier(none,'VV'),identifier(none,'SS'))),implication(rodinpos('ListLawsMC_inf',inv48,'_'),equal(none,identifier(none,'SS'),identifier(none,'VV')),equal(none,card(none,identifier(none,'SS')),card(none,identifier(none,'VV')))),conjunct(rodinpos('ListLawsMC_inf',inv49,'\140\'),less_equal(none,card(none,intersection(none,identifier(none,'SS'),identifier(none,'VV'))),card(none,identifier(none,'SS'))),less_equal(none,card(none,intersection(none,identifier(none,'SS'),identifier(none,'VV'))),card(none,identifier(none,'VV')))),conjunct(rodinpos('ListLawsMC_inf',inv50,a),disjunct(none,subset_strict(none,identifier(none,'SS'),identifier(none,'VV')),negation(none,subset_strict(none,identifier(none,'SS'),identifier(none,'VV')))),conjunct(none,negation(none,conjunct(none,subset_strict(none,identifier(none,'SS'),identifier(none,'VV')),negation(none,subset_strict(none,identifier(none,'SS'),identifier(none,'VV'))))),conjunct(none,disjunct(none,subset(none,identifier(none,'SS'),identifier(none,'VV')),negation(none,subset(none,identifier(none,'SS'),identifier(none,'VV')))),conjunct(none,negation(none,conjunct(none,subset(none,identifier(none,'SS'),identifier(none,'VV')),negation(none,subset(none,identifier(none,'SS'),identifier(none,'VV'))))),conjunct(none,disjunct(none,not_subset_strict(none,identifier(none,'SS'),identifier(none,'VV')),negation(none,not_subset_strict(none,identifier(none,'SS'),identifier(none,'VV')))),conjunct(none,negation(none,conjunct(none,not_subset_strict(none,identifier(none,'SS'),identifier(none,'VV')),negation(none,not_subset_strict(none,identifier(none,'SS'),identifier(none,'VV'))))),conjunct(none,disjunct(none,not_subset(none,identifier(none,'SS'),identifier(none,'VV')),negation(none,not_subset(none,identifier(none,'SS'),identifier(none,'VV')))),negation(none,conjunct(none,not_subset(none,identifier(none,'SS'),identifier(none,'VV')),negation(none,not_subset(none,identifier(none,'SS'),identifier(none,'VV')))))))))))),conjunct(rodinpos('ListLawsMC_inf',inv51,b),disjunct(none,not_member(none,identifier(none,'SS'),pow_subset(none,identifier(none,'TT'))),negation(none,not_member(none,identifier(none,'SS'),pow_subset(none,identifier(none,'TT'))))),conjunct(none,negation(none,conjunct(none,not_member(none,identifier(none,'SS'),pow_subset(none,identifier(none,'TT'))),negation(none,not_member(none,identifier(none,'SS'),pow_subset(none,identifier(none,'TT')))))),conjunct(none,disjunct(none,member(none,identifier(none,'SS'),pow_subset(none,identifier(none,'TT'))),negation(none,member(none,identifier(none,'SS'),pow_subset(none,identifier(none,'TT'))))),conjunct(none,negation(none,conjunct(none,member(none,identifier(none,'SS'),pow_subset(none,identifier(none,'TT'))),negation(none,member(none,identifier(none,'SS'),pow_subset(none,identifier(none,'TT')))))),equal(none,pow1_subset(none,identifier(none,'SS')),set_subtraction(none,pow_subset(none,identifier(none,'SS')),set_extension(none,[typeof(none,empty_set(none),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[])))]))))))),conjunct(rodinpos('ListLawsMC_inf',inv52,c),equal(none,card(none,pow1_subset(none,identifier(none,'SS'))),minus(none,card(none,pow_subset(none,identifier(none,'SS'))),integer(none,1))),conjunct(none,equal(none,card(none,set_subtraction(none,pow_subset(none,identifier(none,'SS')),set_extension(none,[typeof(none,empty_set(none),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[])))]))),minus(none,card(none,pow_subset(none,identifier(none,'SS'))),integer(none,1))),equal(none,union(none,set_subtraction(none,pow_subset(none,identifier(none,'SS')),set_extension(none,[typeof(none,empty_set(none),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[])))])),set_extension(none,[typeof(none,empty_set(none),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[])))])),pow_subset(none,identifier(none,'SS'))))),equal(rodinpos('ListLawsMC_inf',inv53,d),quantified_union(none,[identifier(none,ss)],conjunct(none,member(none,identifier(none,ss),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[]))),subset(none,identifier(none,ss),identifier(none,'SS'))),identifier(none,ss)),identifier(none,'SS')),equivalence(rodinpos('ListLawsMC_inf',inv54,e),not_equal(none,card(none,identifier(none,'SS')),integer(none,1)),equal(none,quantified_union(none,[identifier(none,ss)],conjunct(none,member(none,identifier(none,ss),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[]))),subset_strict(none,identifier(none,ss),identifier(none,'SS'))),identifier(none,ss)),identifier(none,'SS'))),equal(rodinpos('ListLawsMC_inf',inv55,f),quantified_intersection(none,[identifier(none,ss)],conjunct(none,member(none,identifier(none,ss),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[]))),subset(none,identifier(none,ss),identifier(none,'SS'))),identifier(none,ss)),typeof(none,empty_set(none),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[])))),conjunct(rodinpos('ListLawsMC_inf',inv56,g),equivalence(none,not_equal(none,intersection(none,identifier(none,'SS'),identifier(none,'TT')),typeof(none,empty_set(none),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[])))),exists(none,[identifier(none,ee)],conjunct(none,member(none,identifier(none,ee),extended_expr(none,'List',[integer_set(none)],[])),conjunct(none,member(none,identifier(none,ee),identifier(none,'SS')),member(none,identifier(none,ee),identifier(none,'TT')))))),conjunct(none,equivalence(none,not_subset(none,identifier(none,'SS'),identifier(none,'TT')),exists(none,[identifier(none,ee)],conjunct(none,member(none,identifier(none,ee),extended_expr(none,'List',[integer_set(none)],[])),conjunct(none,member(none,identifier(none,ee),identifier(none,'SS')),not_member(none,identifier(none,ee),identifier(none,'TT')))))),equivalence(none,subset_strict(none,identifier(none,'SS'),identifier(none,'TT')),conjunct(none,subset(none,identifier(none,'SS'),identifier(none,'TT')),exists(none,[identifier(none,ee)],conjunct(none,member(none,identifier(none,ee),extended_expr(none,'List',[integer_set(none)],[])),conjunct(none,member(none,identifier(none,ee),identifier(none,'TT')),not_member(none,identifier(none,ee),identifier(none,'SS'))))))))),conjunct(rodinpos('ListLawsMC_inf',inv57,h),equivalence(none,member(none,identifier(none,'SS'),pow_subset(none,identifier(none,'TT'))),subset(none,identifier(none,'SS'),identifier(none,'TT'))),conjunct(none,equivalence(none,equal(none,identifier(none,'SS'),identifier(none,'TT')),equal(none,pow_subset(none,identifier(none,'SS')),pow_subset(none,identifier(none,'TT')))),equal(none,pow_subset(none,set_subtraction(none,identifier(none,'SS'),identifier(none,'TT'))),event_b_comprehension_set(none,[identifier(none,xx)],identifier(none,xx),conjunct(none,member(none,identifier(none,xx),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[]))),conjunct(none,subset(none,identifier(none,xx),identifier(none,'SS')),equal(none,intersection(none,identifier(none,xx),identifier(none,'TT')),typeof(none,empty_set(none),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[])))))))))),conjunct(rodinpos('ListLawsMC_inf',inv58,i),equal(none,general_intersection(none,set_extension(none,[identifier(none,'SS')])),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,member(none,identifier(none,x),extended_expr(none,'List',[integer_set(none)],[])),forall(none,[identifier(none,y)],implication(none,conjunct(none,member(none,identifier(none,y),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[]))),member(none,identifier(none,y),set_extension(none,[identifier(none,'SS')]))),member(none,identifier(none,x),identifier(none,y))))))),conjunct(none,equal(none,general_intersection(none,set_extension(none,[identifier(none,'SS'),identifier(none,'TT')])),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,member(none,identifier(none,x),extended_expr(none,'List',[integer_set(none)],[])),forall(none,[identifier(none,y)],implication(none,conjunct(none,member(none,identifier(none,y),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[]))),member(none,identifier(none,y),set_extension(none,[identifier(none,'SS'),identifier(none,'TT')]))),member(none,identifier(none,x),identifier(none,y))))))),conjunct(none,equal(none,general_intersection(none,set_extension(none,[identifier(none,'SS'),identifier(none,'TT'),identifier(none,'VV')])),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,member(none,identifier(none,x),extended_expr(none,'List',[integer_set(none)],[])),forall(none,[identifier(none,y)],implication(none,conjunct(none,member(none,identifier(none,y),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[]))),member(none,identifier(none,y),set_extension(none,[identifier(none,'SS'),identifier(none,'TT'),identifier(none,'VV')]))),member(none,identifier(none,x),identifier(none,y))))))),conjunct(none,equal(none,general_union(none,typeof(none,empty_set(none),pow_subset(none,pow_subset(none,pow_subset(none,extended_expr(none,'List',[integer_set(none)],[])))))),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,member(none,identifier(none,x),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[]))),conjunct(none,subset(none,identifier(none,x),identifier(none,'TT')),exists(none,[identifier(none,y)],conjunct(none,member(none,identifier(none,y),pow_subset(none,pow_subset(none,extended_expr(none,'List',[integer_set(none)],[])))),conjunct(none,member(none,identifier(none,y),typeof(none,empty_set(none),pow_subset(none,pow_subset(none,pow_subset(none,extended_expr(none,'List',[integer_set(none)],[])))))),member(none,identifier(none,x),identifier(none,y))))))))),conjunct(none,equal(none,general_union(none,set_extension(none,[identifier(none,'SS')])),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,member(none,identifier(none,x),extended_expr(none,'List',[integer_set(none)],[])),exists(none,[identifier(none,y)],conjunct(none,member(none,identifier(none,y),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[]))),conjunct(none,member(none,identifier(none,y),set_extension(none,[identifier(none,'SS')])),member(none,identifier(none,x),identifier(none,y)))))))),conjunct(none,equal(none,general_union(none,set_extension(none,[identifier(none,'SS'),identifier(none,'TT')])),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,member(none,identifier(none,x),extended_expr(none,'List',[integer_set(none)],[])),exists(none,[identifier(none,y)],conjunct(none,member(none,identifier(none,y),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[]))),conjunct(none,member(none,identifier(none,y),set_extension(none,[identifier(none,'SS'),identifier(none,'TT')])),member(none,identifier(none,x),identifier(none,y)))))))),equal(none,general_union(none,set_extension(none,[identifier(none,'SS'),identifier(none,'TT'),identifier(none,'VV')])),event_b_comprehension_set(none,[identifier(none,x)],identifier(none,x),conjunct(none,member(none,identifier(none,x),extended_expr(none,'List',[integer_set(none)],[])),exists(none,[identifier(none,y)],conjunct(none,member(none,identifier(none,y),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[]))),conjunct(none,member(none,identifier(none,y),set_extension(none,[identifier(none,'SS'),identifier(none,'TT'),identifier(none,'VV')])),member(none,identifier(none,x),identifier(none,y)))))))))))))),conjunct(rodinpos('ListLawsMC_inf',inv59,j),equal(none,general_intersection(none,set_extension(none,[identifier(none,'SS')])),identifier(none,'SS')),conjunct(none,equal(none,general_union(none,set_extension(none,[identifier(none,'SS')])),identifier(none,'SS')),conjunct(none,equal(none,general_intersection(none,set_extension(none,[identifier(none,'SS'),identifier(none,'TT')])),intersection(none,identifier(none,'SS'),identifier(none,'TT'))),equal(none,general_union(none,set_extension(none,[identifier(none,'SS'),identifier(none,'TT')])),union(none,identifier(none,'SS'),identifier(none,'TT')))))),subset(rodinpos('ListLawsMC_inf',inv60,l),identifier(none,'SS'),typeof(none,extended_expr(none,'List',[interval(none,integer(none,-2),integer(none,4))],[]),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[]))))]),theorems(none,[]),events(none,[event(rodinpos('ListLawsMC_inf','INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos('ListLawsMC_inf',act1,'\''),[identifier(none,'SS')],[typeof(none,empty_set(none),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[])))]),assign(rodinpos('ListLawsMC_inf',act2,'('),[identifier(none,'TT')],[typeof(none,empty_set(none),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[])))]),assign(rodinpos('ListLawsMC_inf',act3,')'),[identifier(none,'VV')],[typeof(none,empty_set(none),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[])))]),assign(rodinpos('ListLawsMC_inf',act4,'*'),[identifier(none,setX)],[typeof(none,extended_expr(none,'List',[integer_set(none)],[]),pow_subset(none,extended_expr(none,'List',[integer_set(none)],[])))])],[]),event(rodinpos('ListLawsMC_inf',add_SS,'.'),add_SS,ordinary(none),[],[identifier(rodinpos('ListLawsMC_inf',[],'\''),s)],[not_member(rodinpos('ListLawsMC_inf',grd1,'('),identifier(none,s),identifier(none,'SS'))],[],[assign(rodinpos('ListLawsMC_inf',act1,')'),[identifier(none,'SS')],[union(none,identifier(none,'SS'),set_extension(none,[identifier(none,s)]))])],[]),event(rodinpos('ListLawsMC_inf',add_TT,'/'),add_TT,ordinary(none),[],[identifier(rodinpos('ListLawsMC_inf',[],'\''),s)],[not_member(rodinpos('ListLawsMC_inf',grd1,'('),identifier(none,s),identifier(none,'TT'))],[],[assign(rodinpos('ListLawsMC_inf',act1,')'),[identifier(none,'TT')],[union(none,identifier(none,'TT'),set_extension(none,[identifier(none,s)]))])],[]),event(rodinpos('ListLawsMC_inf',add_VV,'0'),add_VV,ordinary(none),[],[identifier(rodinpos('ListLawsMC_inf',[],'\''),s)],[not_member(rodinpos('ListLawsMC_inf',grd1,'('),identifier(none,s),identifier(none,'VV'))],[],[assign(rodinpos('ListLawsMC_inf',act1,')'),[identifier(none,'VV')],[union(none,identifier(none,'VV'),set_extension(none,[identifier(none,s)]))])],[]),event(rodinpos('ListLawsMC_inf',set_SS_max,k),set_SS_max,ordinary(none),[],[],[disjunct(rodinpos('ListLawsMC_inf',grd1,'('),equal(none,integer(none,1),integer(none,1)),not_equal(none,identifier(none,'SS'),identifier(none,setX)))],[],[assign(rodinpos('ListLawsMC_inf',act1,'\''),[identifier(none,'SS')],[identifier(none,setX)])],[]),event(rodinpos('ListLawsMC_inf',set_TT_max,m),set_TT_max,ordinary(none),[],[],[],[],[assign(rodinpos('ListLawsMC_inf',act1,'\''),[identifier(none,'TT')],[identifier(none,setX)])],[]),event(rodinpos('ListLawsMC_inf',set_VV_max,n),set_VV_max,ordinary(none),[],[],[],[],[assign(rodinpos('ListLawsMC_inf',act1,'\''),[identifier(none,'VV')],[identifier(none,setX)])],[])])])],[],[exporter_version(3),po('ListLawsMC_inf','Well-definedness of Invariant',[invariant(inv42)],false),po('ListLawsMC_inf','Well-definedness of Invariant',[invariant(inv43)],false),po('ListLawsMC_inf','Well-definedness of Invariant',[invariant(inv44)],false),po('ListLawsMC_inf','Well-definedness of Invariant',[invariant(inv45)],false),po('ListLawsMC_inf','Well-definedness of Invariant',[invariant(inv46)],false),po('ListLawsMC_inf','Well-definedness of Invariant',[invariant(inv47)],false),po('ListLawsMC_inf','Well-definedness of Invariant',[invariant(inv48)],false),po('ListLawsMC_inf','Well-definedness of Invariant',[invariant(inv49)],false),po('ListLawsMC_inf','Well-definedness of Invariant',[invariant(inv52)],false),po('ListLawsMC_inf','Well-definedness of Invariant',[invariant(inv54)],false),po('ListLawsMC_inf','Well-definedness of Invariant',[invariant(inv55)],false),po('ListLawsMC_inf','Well-definedness of Invariant',[invariant(inv58)],false),po('ListLawsMC_inf','Well-definedness of Invariant',[invariant(inv59)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv2)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv4)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv5)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv6)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv7)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv8)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv9)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv10)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv11)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv12)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv13)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv14)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv15)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv16)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv17)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv18)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv19)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv20)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv21)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv22)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv23)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv24)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv25)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv26)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv27)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv28)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv29)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv30)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv31)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv32)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv33)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv34)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv35)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv36)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv37)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv38)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv39)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv40)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv41)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv42)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv43)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv44)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv45)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv46)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv47)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv48)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv49)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv50)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv51)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv52)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv53)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv54)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv55)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv56)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv57)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv58)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv59)],false),po('ListLawsMC_inf','Invariant establishment',[event('INITIALISATION'),invariant(inv60)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv2)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv4)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv5)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv6)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv7)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv8)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv9)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv10)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv11)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv12)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv13)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv14)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv15)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv16)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv17)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv18)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv19)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv20)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv21)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv22)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv23)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv24)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv25)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv26)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv27)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv28)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv29)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv30)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv31)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv32)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv33)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv34)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv35)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv36)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv37)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv38)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv39)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv40)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv41)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv42)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv43)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv44)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv45)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv46)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv47)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv48)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv49)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv50)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv51)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv52)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv53)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv54)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv55)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv56)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv57)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv58)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv59)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_SS),invariant(inv60)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv2)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv6)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv7)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv8)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv9)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv10)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv11)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv12)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv13)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv14)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv15)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv16)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv17)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv18)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv19)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv20)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv21)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv22)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv23)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv24)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv25)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv26)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv27)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv28)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv29)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv31)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv32)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv34)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv51)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv56)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv57)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv58)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_TT),invariant(inv59)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv3)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv7)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv8)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv9)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv12)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv13)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv14)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv15)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv16)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv17)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv19)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv21)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv24)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv28)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv30)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv31)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv32)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv33)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv35)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv36)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv37)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv38)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv39)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv40)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv41)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv42)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv43)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv44)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv45)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv46)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv47)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv48)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv49)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv50)],false),po('ListLawsMC_inf','Invariant preservation',[event(add_VV),invariant(inv58)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv2)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv4)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv5)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv6)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv7)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv8)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv9)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv10)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv11)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv12)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv13)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv14)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv15)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv16)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv17)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv18)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv19)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv20)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv21)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv22)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv23)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv24)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv25)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv26)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv27)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv28)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv29)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv30)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv31)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv32)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv33)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv34)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv35)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv36)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv37)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv38)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv39)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv40)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv41)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv42)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv43)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv44)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv45)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv46)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv47)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv48)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv49)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv50)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv51)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv52)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv53)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv54)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv55)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv56)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv57)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv58)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv59)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_SS_max),invariant(inv60)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv2)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv6)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv7)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv8)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv9)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv10)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv11)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv12)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv13)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv14)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv15)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv16)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv17)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv18)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv19)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv20)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv21)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv22)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv23)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv24)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv25)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv26)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv27)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv28)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv29)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv31)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv32)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv34)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv51)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv56)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv57)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv58)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_TT_max),invariant(inv59)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv3)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv7)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv8)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv9)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv12)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv13)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv14)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv15)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv16)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv17)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv19)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv21)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv24)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv28)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv30)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv31)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv32)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv33)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv35)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv36)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv37)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv38)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv39)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv40)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv41)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv42)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv43)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv44)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv45)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv46)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv47)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv48)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv49)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv50)],false),po('ListLawsMC_inf','Invariant preservation',[event(set_VV_max),invariant(inv58)],false),theory(theory_name('MathExtensions','List'),[],['S','T'],[datatype('List',[identifier(none,'T')],[constructor(nil,[]),constructor(cons,[destructor(head,identifier(none,'T')),destructor(tail,typeof(none,extended_expr(none,'List',[identifier(none,'T')],[]),pow_subset(none,extended_expr(none,'List',[identifier(none,'T')],[]))))])])],[operator(listSize,[argument(l,typeof(none,extended_expr(none,'List',[identifier(none,'T')],[]),pow_subset(none,extended_expr(none,'List',[identifier(none,'T')],[]))))],truth(none),[],[case(l,[],typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[])),integer(none,0)),case(l,[l0,x],extended_expr(none,cons,[identifier(none,x),identifier(none,l0)],[]),add(none,integer(none,1),extended_expr(none,listSize,[identifier(none,l0)],[])))]),operator(append,[argument(l,typeof(none,extended_expr(none,'List',[identifier(none,'T')],[]),pow_subset(none,extended_expr(none,'List',[identifier(none,'T')],[])))),argument(x,identifier(none,'T'))],truth(none),[],[case(l,[],typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[])),extended_expr(none,cons,[identifier(none,x),typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[]))],[])),case(l,[l0,x0],extended_expr(none,cons,[identifier(none,x0),identifier(none,l0)],[]),extended_expr(none,cons,[identifier(none,x0),extended_expr(none,append,[identifier(none,l0),identifier(none,x)],[])],[]))]),operator(rev,[argument(l,typeof(none,extended_expr(none,'List',[identifier(none,'T')],[]),pow_subset(none,extended_expr(none,'List',[identifier(none,'T')],[]))))],truth(none),[],[case(l,[],typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[])),typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[]))),case(l,[l0,x],extended_expr(none,cons,[identifier(none,x),identifier(none,l0)],[]),extended_expr(none,append,[extended_expr(none,rev,[identifier(none,l0)],[]),identifier(none,x)],[]))]),operator(comp,[argument(l,typeof(none,extended_expr(none,'List',[identifier(none,'T')],[]),pow_subset(none,extended_expr(none,'List',[identifier(none,'T')],[])))),argument(f,pow_subset(none,cartesian_product(none,identifier(none,'T'),identifier(none,'S'))))],truth(none),[],[case(l,[],typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[])),typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'S')],[]))),case(l,[l0,x],extended_expr(none,cons,[identifier(none,x),identifier(none,l0)],[]),extended_expr(none,cons,[function(none,identifier(none,f),[identifier(none,x)]),extended_expr(none,comp,[identifier(none,l0),identifier(none,f)],[])],[]))]),operator(conc,[argument(l1,typeof(none,extended_expr(none,'List',[identifier(none,'T')],[]),pow_subset(none,extended_expr(none,'List',[identifier(none,'T')],[])))),argument(l2,typeof(none,extended_expr(none,'List',[identifier(none,'T')],[]),pow_subset(none,extended_expr(none,'List',[identifier(none,'T')],[]))))],truth(none),[],[case(l1,[],typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[])),identifier(none,l2)),case(l1,[l0,x],extended_expr(none,cons,[identifier(none,x),identifier(none,l0)],[]),extended_expr(none,cons,[identifier(none,x),extended_expr(none,conc,[identifier(none,l0),identifier(none,l2)],[])],[]))]),operator(flatten,[argument(l,typeof(none,extended_expr(none,'List',[typeof(none,extended_expr(none,'List',[identifier(none,'T')],[]),pow_subset(none,extended_expr(none,'List',[identifier(none,'T')],[])))],[]),pow_subset(none,extended_expr(none,'List',[extended_expr(none,'List',[identifier(none,'T')],[])],[]))))],truth(none),[],[case(l,[],typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[extended_expr(none,'List',[identifier(none,'T')],[])],[])),typeof(none,extended_expr(none,nil,[],[]),extended_expr(none,'List',[identifier(none,'T')],[]))),case(l,[l0,ll0],extended_expr(none,cons,[identifier(none,l0),identifier(none,ll0)],[]),extended_expr(none,conc,[identifier(none,l0),extended_expr(none,flatten,[identifier(none,ll0)],[])],[]))])],[],[]),theory(theory_name('Laws','Pairs'),[],['T'],[datatype('Pair',[identifier(none,'T')],[constructor(mk_Pair,[destructor(lft,identifier(none,'T')),destructor(rht,identifier(none,'T'))])])],[],[],[])],_Error)).
2