equal
deleted
inserted
replaced
100 from x map1 |
100 from x map1 |
101 have "\<forall>x \<in> set (?map ss1). x <=_r ?sum ss1" |
101 have "\<forall>x \<in> set (?map ss1). x <=_r ?sum ss1" |
102 by clarify (rule pp_ub1) |
102 by clarify (rule pp_ub1) |
103 with sum have "\<forall>x \<in> set (?map ss1). x <=_r ?s1" by simp |
103 with sum have "\<forall>x \<in> set (?map ss1). x <=_r ?s1" by simp |
104 with less have "\<forall>x \<in> set (?map ss2). x <=_r ?s1" |
104 with less have "\<forall>x \<in> set (?map ss2). x <=_r ?s1" |
105 by (fastsimp dest!: mapD lesub_step_typeD intro: trans_r) |
105 by (fastforce dest!: mapD lesub_step_typeD intro: trans_r) |
106 moreover |
106 moreover |
107 from map1 x have "x <=_r (?sum ss1)" by (rule pp_ub2) |
107 from map1 x have "x <=_r (?sum ss1)" by (rule pp_ub2) |
108 with sum have "x <=_r ?s1" by simp |
108 with sum have "x <=_r ?s1" by simp |
109 moreover |
109 moreover |
110 from ss2 have "set (?map ss2) \<subseteq> A" by auto |
110 from ss2 have "set (?map ss2) \<subseteq> A" by auto |