wneuper/isa: test/Tools/isac/traces/trace-minus_mult_left-isa.txt@f6e98785473f (annotated)

walther@60343	1	# rls: make_polynomial_in on: - 6 + - 5 * x + x \<up> 3 + - 1 * x \<up> 2 + - 1 * x \<up> 3 +
walther@60343	2	- 14 * x \<up> 2
walther@60343	3	## rls: expand_poly on: - 6 + - 5 * x + x \<up> 3 + - 1 * x \<up> 2 + - 1 * x \<up> 3 +
walther@60343	4	- 14 * x \<up> 2
walther@60343	5	### try thm: "distrib_right"
walther@60343	6	### try thm: "distrib_left"
walther@60343	7	### try thm: "real_plus_binom_pow2"
walther@60343	8	### try thm: "real_minus_binom_pow2_p"
walther@60343	9	### try thm: "real_plus_minus_binom1_p"
walther@60343	10	### try thm: "real_plus_minus_binom2_p"
walther@60343	11	### try thm: "minus_minus"
walther@60343	12	### try thm: "real_diff_minus"
walther@60343	13	### try thm: "real_mult_minus1_sym"
walther@60343	14	#### eval asms: "\<lbrakk>\<not> matches (- 1 * ?x) 14; \<not> (14 is_num)\<rbrakk>
walther@60343	15	\<Longrightarrow> - 14 = - 1 * 14"
walther@60343	16	##### rls: powers_erls on: \<not> (14 is_num)
walther@60343	17	###### try calc: "Prog_Expr.matches"
walther@60343	18	###### try calc: "Prog_Expr.is_atom"
walther@60343	19	###### try calc: "Prog_Expr.is_num"
walther@60343	20	####### eval asms: "(14 is_num) = True"
walther@60343	21	###### calc. to: \<not> True
walther@60343	22	###### try calc: "Prog_Expr.is_num"
walther@60343	23	###### try calc: "Prog_Expr.is_even"
walther@60343	24	###### try calc: "Orderings.ord_class.less"
walther@60343	25	###### try thm: "not_false"
walther@60343	26	###### try thm: "not_true"
walther@60343	27	####### eval asms: "(\<not> True) = False"
walther@60343	28	###### rewrites to: "False"
walther@60343	29	###### try thm: "not_true"
walther@60343	30	###### try calc: "Groups.plus_class.plus"
walther@60343	31	###### try calc: "Prog_Expr.matches"
walther@60343	32	###### try calc: "Prog_Expr.is_atom"
walther@60343	33	###### try calc: "Prog_Expr.is_num"
walther@60343	34	###### try calc: "Prog_Expr.is_even"
walther@60343	35	###### try calc: "Orderings.ord_class.less"
walther@60343	36	###### try thm: "not_false"
walther@60343	37	###### try thm: "not_true"
walther@60343	38	###### try calc: "Groups.plus_class.plus"
walther@60343	39	#### asms false: [\<not> (14 is_num), \<not> matches (- 1 * ?x) 14]
walther@60343	40	#### eval asms: "\<lbrakk>\<not> matches (- 1 * ?x) 1; \<not> (1 is_num)\<rbrakk>
walther@60343	41	\<Longrightarrow> - 1 = - 1 * 1"
walther@60343	42	##### rls: powers_erls on: \<not> (1 is_num)
walther@60343	43	###### try calc: "Prog_Expr.matches"
walther@60343	44	###### try calc: "Prog_Expr.is_atom"
walther@60343	45	###### try calc: "Prog_Expr.is_num"
walther@60343	46	####### eval asms: "(1 is_num) = True"
walther@60343	47	###### calc. to: \<not> True
walther@60343	48	###### try calc: "Prog_Expr.is_num"
walther@60343	49	###### try calc: "Prog_Expr.is_even"
walther@60343	50	###### try calc: "Orderings.ord_class.less"
walther@60343	51	###### try thm: "not_false"
walther@60343	52	###### try thm: "not_true"
walther@60343	53	####### eval asms: "(\<not> True) = False"
walther@60343	54	###### rewrites to: "False"
walther@60343	55	###### try thm: "not_true"
walther@60343	56	###### try calc: "Groups.plus_class.plus"
walther@60343	57	###### try calc: "Prog_Expr.matches"
walther@60343	58	###### try calc: "Prog_Expr.is_atom"
walther@60343	59	###### try calc: "Prog_Expr.is_num"
walther@60343	60	###### try calc: "Prog_Expr.is_even"
walther@60343	61	###### try calc: "Orderings.ord_class.less"
walther@60343	62	###### try thm: "not_false"
walther@60343	63	###### try thm: "not_true"
walther@60343	64	###### try calc: "Groups.plus_class.plus"
walther@60343	65	#### asms false: [\<not> (1 is_num), \<not> matches (- 1 * ?x) 1]
walther@60343	66	#### eval asms: "\<lbrakk>\<not> matches (- 1 * ?x) 1; \<not> (1 is_num)\<rbrakk>
walther@60343	67	\<Longrightarrow> - 1 = - 1 * 1"
walther@60343	68	##### rls: powers_erls on: \<not> (1 is_num)
walther@60343	69	###### try calc: "Prog_Expr.matches"
walther@60343	70	###### try calc: "Prog_Expr.is_atom"
walther@60343	71	###### try calc: "Prog_Expr.is_num"
walther@60343	72	####### eval asms: "(1 is_num) = True"
walther@60343	73	###### calc. to: \<not> True
walther@60343	74	###### try calc: "Prog_Expr.is_num"
walther@60343	75	###### try calc: "Prog_Expr.is_even"
walther@60343	76	###### try calc: "Orderings.ord_class.less"
walther@60343	77	###### try thm: "not_false"
walther@60343	78	###### try thm: "not_true"
walther@60343	79	####### eval asms: "(\<not> True) = False"
walther@60343	80	###### rewrites to: "False"
walther@60343	81	###### try thm: "not_true"
walther@60343	82	###### try calc: "Groups.plus_class.plus"
walther@60343	83	###### try calc: "Prog_Expr.matches"
walther@60343	84	###### try calc: "Prog_Expr.is_atom"
walther@60343	85	###### try calc: "Prog_Expr.is_num"
walther@60343	86	###### try calc: "Prog_Expr.is_even"
walther@60343	87	###### try calc: "Orderings.ord_class.less"
walther@60343	88	###### try thm: "not_false"
walther@60343	89	###### try thm: "not_true"
walther@60343	90	###### try calc: "Groups.plus_class.plus"
walther@60343	91	#### asms false: [\<not> (1 is_num), \<not> matches (- 1 * ?x) 1]
walther@60343	92	#### eval asms: "\<lbrakk>\<not> matches (- 1 * ?x) 5; \<not> (5 is_num)\<rbrakk>
walther@60343	93	\<Longrightarrow> - 5 = - 1 * 5"
walther@60343	94	##### rls: powers_erls on: \<not> (5 is_num)
walther@60343	95	###### try calc: "Prog_Expr.matches"
walther@60343	96	###### try calc: "Prog_Expr.is_atom"
walther@60343	97	###### try calc: "Prog_Expr.is_num"
walther@60343	98	####### eval asms: "(5 is_num) = True"
walther@60343	99	###### calc. to: \<not> True
walther@60343	100	###### try calc: "Prog_Expr.is_num"
walther@60343	101	###### try calc: "Prog_Expr.is_even"
walther@60343	102	###### try calc: "Orderings.ord_class.less"
walther@60343	103	###### try thm: "not_false"
walther@60343	104	###### try thm: "not_true"
walther@60343	105	####### eval asms: "(\<not> True) = False"
walther@60343	106	###### rewrites to: "False"
walther@60343	107	###### try thm: "not_true"
walther@60343	108	###### try calc: "Groups.plus_class.plus"
walther@60343	109	###### try calc: "Prog_Expr.matches"
walther@60343	110	###### try calc: "Prog_Expr.is_atom"
walther@60343	111	###### try calc: "Prog_Expr.is_num"
walther@60343	112	###### try calc: "Prog_Expr.is_even"
walther@60343	113	###### try calc: "Orderings.ord_class.less"
walther@60343	114	###### try thm: "not_false"
walther@60343	115	###### try thm: "not_true"
walther@60343	116	###### try calc: "Groups.plus_class.plus"
walther@60343	117	#### asms false: [\<not> (5 is_num), \<not> matches (- 1 * ?x) 5]
walther@60343	118	#### eval asms: "\<lbrakk>\<not> matches (- 1 * ?x) 6; \<not> (6 is_num)\<rbrakk>
walther@60343	119	\<Longrightarrow> - 6 = - 1 * 6"
walther@60343	120	##### rls: powers_erls on: \<not> (6 is_num)
walther@60343	121	###### try calc: "Prog_Expr.matches"
walther@60343	122	###### try calc: "Prog_Expr.is_atom"
walther@60343	123	###### try calc: "Prog_Expr.is_num"
walther@60343	124	####### eval asms: "(6 is_num) = True"
walther@60343	125	###### calc. to: \<not> True
walther@60343	126	###### try calc: "Prog_Expr.is_num"
walther@60343	127	###### try calc: "Prog_Expr.is_even"
walther@60343	128	###### try calc: "Orderings.ord_class.less"
walther@60343	129	###### try thm: "not_false"
walther@60343	130	###### try thm: "not_true"
walther@60343	131	####### eval asms: "(\<not> True) = False"
walther@60343	132	###### rewrites to: "False"
walther@60343	133	###### try thm: "not_true"
walther@60343	134	###### try calc: "Groups.plus_class.plus"
walther@60343	135	###### try calc: "Prog_Expr.matches"
walther@60343	136	###### try calc: "Prog_Expr.is_atom"
walther@60343	137	###### try calc: "Prog_Expr.is_num"
walther@60343	138	###### try calc: "Prog_Expr.is_even"
walther@60343	139	###### try calc: "Orderings.ord_class.less"
walther@60343	140	###### try thm: "not_false"
walther@60343	141	###### try thm: "not_true"
walther@60343	142	###### try calc: "Groups.plus_class.plus"
walther@60343	143	#### asms false: [\<not> (6 is_num), \<not> matches (- 1 * ?x) 6]
walther@60343	144	## rls: order_add_mult_in on: - 6 + - 5 * x + x \<up> 3 + - 1 * x \<up> 2 + - 1 * x \<up> 3 +
walther@60343	145	- 14 * x \<up> 2
walther@60343	146	### try thm: "mult.commute"
walther@60343	147	#### eval asms: "- 14 * x \<up> 2 = x \<up> 2 * - 14"
walther@60343	148	### not >: "- 14 * x \<up> 2" > "x \<up> 2 * - 14"
walther@60343	149	#### eval asms: "- 1 * x \<up> 3 = x \<up> 3 * - 1"
walther@60343	150	### not >: "- 1 * x \<up> 3" > "x \<up> 3 * - 1"
walther@60343	151	#### eval asms: "- 1 * x \<up> 2 = x \<up> 2 * - 1"
walther@60343	152	### not >: "- 1 * x \<up> 2" > "x \<up> 2 * - 1"
walther@60343	153	#### eval asms: "- 5 * x = x * - 5"
walther@60343	154	### not >: "- 5 * x" > "x * - 5"
walther@60343	155	### try thm: "real_mult_left_commute"
walther@60343	156	### try thm: "mult.assoc"
walther@60343	157	### try thm: "add.commute"
walther@60343	158	#### eval asms: "- 6 + - 5 * x + x \<up> 3 + - 1 * x \<up> 2 + - 1 * x \<up> 3 + - 14 * x \<up> 2 =
walther@60343	159	- 14 * x \<up> 2 + (- 6 + - 5 * x + x \<up> 3 + - 1 * x \<up> 2 + - 1 * x \<up> 3)"
walther@60343	160	### rewrites to: "- 14 * x \<up> 2 + (- 6 + - 5 * x + x \<up> 3 + - 1 * x \<up> 2 + - 1 * x \<up> 3)"
walther@60343	161	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
walther@60343	162	### try thm: "add.commute"
walther@60343	163	#### eval asms: "- 14 * x \<up> 2 + (- 6 + - 5 * x + x \<up> 3 + - 1 * x \<up> 2 + - 1 * x \<up> 3) =
walther@60343	164	- 6 + - 5 * x + x \<up> 3 + - 1 * x \<up> 2 + - 1 * x \<up> 3 + - 14 * x \<up> 2"
walther@60343	165	### not >: "- 14 * x \<up> 2 +
walther@60343	166	(- 6 + - 5 * x + x \<up> 3 + - 1 * x \<up> 2 + - 1 * x \<up> 3)" > "- 6 + - 5 * x + x \<up> 3 + - 1 * x \<up> 2 + - 1 * x \<up> 3 +
walther@60343	167	- 14 * x \<up> 2"
walther@60343	168	#### eval asms: "- 6 + - 5 * x + x \<up> 3 + - 1 * x \<up> 2 + - 1 * x \<up> 3 =
walther@60343	169	- 1 * x \<up> 3 + (- 6 + - 5 * x + x \<up> 3 + - 1 * x \<up> 2)"
walther@60343	170	### rewrites to: "- 14 * x \<up> 2 + (- 1 * x \<up> 3 + (- 6 + - 5 * x + x \<up> 3 + - 1 * x \<up> 2))"
walther@60343	171	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
walther@60343	172	### try thm: "add.commute"
walther@60343	173	#### eval asms: "- 14 * x \<up> 2 +
walther@60343	174	(- 1 * x \<up> 3 + (- 6 + - 5 * x + x \<up> 3 + - 1 * x \<up> 2)) =
walther@60343	175	- 1 * x \<up> 3 + (- 6 + - 5 * x + x \<up> 3 + - 1 * x \<up> 2) +
walther@60343	176	- 14 * x \<up> 2"
walther@60343	177	### not >: "- 14 * x \<up> 2 +
walther@60343	178	(- 1 * x \<up> 3 + (- 6 + - 5 * x + x \<up> 3 + - 1 * x \<up> 2))" > "- 1 * x \<up> 3 + (- 6 + - 5 * x + x \<up> 3 + - 1 * x \<up> 2) +
walther@60343	179	- 14 * x \<up> 2"
walther@60343	180	#### eval asms: "- 1 * x \<up> 3 + (- 6 + - 5 * x + x \<up> 3 + - 1 * x \<up> 2) =
walther@60343	181	- 6 + - 5 * x + x \<up> 3 + - 1 * x \<up> 2 + - 1 * x \<up> 3"
walther@60343	182	### not >: "- 1 * x \<up> 3 + (- 6 + - 5 * x + x \<up> 3 + - 1 * x \<up> 2)" > "- 6 + - 5 * x + x \<up> 3 + - 1 * x \<up> 2 + - 1 * x \<up> 3"
walther@60343	183	#### eval asms: "- 6 + - 5 * x + x \<up> 3 + - 1 * x \<up> 2 =
walther@60343	184	- 1 * x \<up> 2 + (- 6 + - 5 * x + x \<up> 3)"
walther@60343	185	### rewrites to: "- 14 * x \<up> 2 + (- 1 * x \<up> 3 + (- 1 * x \<up> 2 + (- 6 + - 5 * x + x \<up> 3)))"
walther@60343	186	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
walther@60343	187	### try thm: "add.commute"
walther@60343	188	#### eval asms: "- 14 * x \<up> 2 +
walther@60343	189	(- 1 * x \<up> 3 + (- 1 * x \<up> 2 + (- 6 + - 5 * x + x \<up> 3))) =
walther@60343	190	- 1 * x \<up> 3 + (- 1 * x \<up> 2 + (- 6 + - 5 * x + x \<up> 3)) +
walther@60343	191	- 14 * x \<up> 2"
walther@60343	192	### not >: "- 14 * x \<up> 2 +
walther@60343	193	(- 1 * x \<up> 3 + (- 1 * x \<up> 2 + (- 6 + - 5 * x + x \<up> 3)))" > "- 1 * x \<up> 3 + (- 1 * x \<up> 2 + (- 6 + - 5 * x + x \<up> 3)) +
walther@60343	194	- 14 * x \<up> 2"
walther@60343	195	#### eval asms: "- 1 * x \<up> 3 + (- 1 * x \<up> 2 + (- 6 + - 5 * x + x \<up> 3)) =
walther@60343	196	- 1 * x \<up> 2 + (- 6 + - 5 * x + x \<up> 3) + - 1 * x \<up> 3"
walther@60343	197	### not >: "- 1 * x \<up> 3 + (- 1 * x \<up> 2 + (- 6 + - 5 * x + x \<up> 3))" > "- 1 * x \<up> 2 + (- 6 + - 5 * x + x \<up> 3) + - 1 * x \<up> 3"
walther@60343	198	#### eval asms: "- 1 * x \<up> 2 + (- 6 + - 5 * x + x \<up> 3) =
walther@60343	199	- 6 + - 5 * x + x \<up> 3 + - 1 * x \<up> 2"
walther@60343	200	### not >: "- 1 * x \<up> 2 + (- 6 + - 5 * x + x \<up> 3)" > "- 6 + - 5 * x + x \<up> 3 + - 1 * x \<up> 2"
walther@60343	201	#### eval asms: "- 6 + - 5 * x + x \<up> 3 = x \<up> 3 + (- 6 + - 5 * x)"
walther@60343	202	### not >: "- 6 + - 5 * x + x \<up> 3" > "x \<up> 3 + (- 6 + - 5 * x)"
walther@60343	203	#### eval asms: "- 6 + - 5 * x = - 5 * x + - 6"
walther@60343	204	### not >: "- 6 + - 5 * x" > "- 5 * x + - 6"
walther@60343	205	### try thm: "add.left_commute"
walther@60343	206	#### eval asms: "- 14 * x \<up> 2 +
walther@60343	207	(- 1 * x \<up> 3 + (- 1 * x \<up> 2 + (- 6 + - 5 * x + x \<up> 3))) =
walther@60343	208	- 1 * x \<up> 3 +
walther@60343	209	(- 14 * x \<up> 2 + (- 1 * x \<up> 2 + (- 6 + - 5 * x + x \<up> 3)))"
walther@60343	210	### not >: "- 14 * x \<up> 2 +
walther@60343	211	(- 1 * x \<up> 3 + (- 1 * x \<up> 2 + (- 6 + - 5 * x + x \<up> 3)))" > "- 1 * x \<up> 3 +
walther@60343	212	(- 14 * x \<up> 2 + (- 1 * x \<up> 2 + (- 6 + - 5 * x + x \<up> 3)))"
walther@60343	213	#### eval asms: "- 1 * x \<up> 3 + (- 1 * x \<up> 2 + (- 6 + - 5 * x + x \<up> 3)) =
walther@60343	214	- 1 * x \<up> 2 + (- 1 * x \<up> 3 + (- 6 + - 5 * x + x \<up> 3))"
walther@60343	215	### rewrites to: "- 14 * x \<up> 2 + (- 1 * x \<up> 2 + (- 1 * x \<up> 3 + (- 6 + - 5 * x + x \<up> 3)))"
walther@60343	216	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
walther@60343	217	### try thm: "add.left_commute"
walther@60343	218	#### eval asms: "- 14 * x \<up> 2 +
walther@60343	219	(- 1 * x \<up> 2 + (- 1 * x \<up> 3 + (- 6 + - 5 * x + x \<up> 3))) =
walther@60343	220	- 1 * x \<up> 2 +
walther@60343	221	(- 14 * x \<up> 2 + (- 1 * x \<up> 3 + (- 6 + - 5 * x + x \<up> 3)))"
walther@60343	222	### rewrites to: "- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (- 1 * x \<up> 3 + (- 6 + - 5 * x + x \<up> 3)))"
walther@60343	223	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
walther@60343	224	### try thm: "add.left_commute"
walther@60343	225	#### eval asms: "- 1 * x \<up> 2 +
walther@60343	226	(- 14 * x \<up> 2 + (- 1 * x \<up> 3 + (- 6 + - 5 * x + x \<up> 3))) =
walther@60343	227	- 14 * x \<up> 2 +
walther@60343	228	(- 1 * x \<up> 2 + (- 1 * x \<up> 3 + (- 6 + - 5 * x + x \<up> 3)))"
walther@60343	229	### not >: "- 1 * x \<up> 2 +
walther@60343	230	(- 14 * x \<up> 2 + (- 1 * x \<up> 3 + (- 6 + - 5 * x + x \<up> 3)))" > "- 14 * x \<up> 2 +
walther@60343	231	(- 1 * x \<up> 2 + (- 1 * x \<up> 3 + (- 6 + - 5 * x + x \<up> 3)))"
walther@60343	232	#### eval asms: "- 14 * x \<up> 2 + (- 1 * x \<up> 3 + (- 6 + - 5 * x + x \<up> 3)) =
walther@60343	233	- 1 * x \<up> 3 + (- 14 * x \<up> 2 + (- 6 + - 5 * x + x \<up> 3))"
walther@60343	234	### not >: "- 14 * x \<up> 2 + (- 1 * x \<up> 3 + (- 6 + - 5 * x + x \<up> 3))" > "- 1 * x \<up> 3 + (- 14 * x \<up> 2 + (- 6 + - 5 * x + x \<up> 3))"
walther@60343	235	#### eval asms: "- 1 * x \<up> 3 + (- 6 + - 5 * x + x \<up> 3) =
walther@60343	236	- 6 + - 5 * x + (- 1 * x \<up> 3 + x \<up> 3)"
walther@60343	237	### rewrites to: "- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (- 6 + - 5 * x + (- 1 * x \<up> 3 + x \<up> 3)))"
walther@60343	238	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
walther@60343	239	### try thm: "add.left_commute"
walther@60343	240	#### eval asms: "- 1 * x \<up> 2 +
walther@60343	241	(- 14 * x \<up> 2 + (- 6 + - 5 * x + (- 1 * x \<up> 3 + x \<up> 3))) =
walther@60343	242	- 14 * x \<up> 2 +
walther@60343	243	(- 1 * x \<up> 2 + (- 6 + - 5 * x + (- 1 * x \<up> 3 + x \<up> 3)))"
walther@60343	244	### not >: "- 1 * x \<up> 2 +
walther@60343	245	(- 14 * x \<up> 2 + (- 6 + - 5 * x + (- 1 * x \<up> 3 + x \<up> 3)))" > "- 14 * x \<up> 2 +
walther@60343	246	(- 1 * x \<up> 2 + (- 6 + - 5 * x + (- 1 * x \<up> 3 + x \<up> 3)))"
walther@60343	247	#### eval asms: "- 14 * x \<up> 2 + (- 6 + - 5 * x + (- 1 * x \<up> 3 + x \<up> 3)) =
walther@60343	248	- 6 + - 5 * x + (- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3))"
walther@60343	249	### rewrites to: "- 1 * x \<up> 2 + (- 6 + - 5 * x + (- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3)))"
walther@60343	250	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
walther@60343	251	### try thm: "add.left_commute"
walther@60343	252	#### eval asms: "- 1 * x \<up> 2 +
walther@60343	253	(- 6 + - 5 * x + (- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3))) =
walther@60343	254	- 6 + - 5 * x +
walther@60343	255	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3)))"
walther@60343	256	### rewrites to: "- 6 + - 5 * x + (- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3)))"
walther@60343	257	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
walther@60343	258	### try thm: "add.left_commute"
walther@60343	259	#### eval asms: "- 6 + - 5 * x +
walther@60343	260	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3))) =
walther@60343	261	- 1 * x \<up> 2 +
walther@60343	262	(- 6 + - 5 * x + (- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3)))"
walther@60343	263	### not >: "- 6 + - 5 * x +
walther@60343	264	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3)))" > "- 1 * x \<up> 2 +
walther@60343	265	(- 6 + - 5 * x + (- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3)))"
walther@60343	266	#### eval asms: "- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3)) =
walther@60343	267	- 14 * x \<up> 2 + (- 1 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3))"
walther@60343	268	### not >: "- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3))" > "- 14 * x \<up> 2 + (- 1 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3))"
walther@60343	269	#### eval asms: "- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3) =
walther@60343	270	- 1 * x \<up> 3 + (- 14 * x \<up> 2 + x \<up> 3)"
walther@60343	271	### not >: "- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3)" > "- 1 * x \<up> 3 + (- 14 * x \<up> 2 + x \<up> 3)"
walther@60343	272	### try thm: "add.assoc"
walther@60343	273	#### eval asms: "- 6 + - 5 * x +
walther@60343	274	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3))) =
walther@60343	275	- 6 +
walther@60343	276	(- 5 * x +
walther@60343	277	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3))))"
walther@60343	278	### rewrites to: "- 6 + (- 5 * x + (- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3))))"
walther@60343	279	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
walther@60343	280	### try thm: "add.assoc"
walther@60343	281	### try thm: "mult.commute"
walther@60343	282	#### eval asms: "- 1 * x \<up> 3 = x \<up> 3 * - 1"
walther@60343	283	### not >: "- 1 * x \<up> 3" > "x \<up> 3 * - 1"
walther@60343	284	#### eval asms: "- 14 * x \<up> 2 = x \<up> 2 * - 14"
walther@60343	285	### not >: "- 14 * x \<up> 2" > "x \<up> 2 * - 14"
walther@60343	286	#### eval asms: "- 1 * x \<up> 2 = x \<up> 2 * - 1"
walther@60343	287	### not >: "- 1 * x \<up> 2" > "x \<up> 2 * - 1"
walther@60343	288	#### eval asms: "- 5 * x = x * - 5"
walther@60343	289	### not >: "- 5 * x" > "x * - 5"
walther@60343	290	### try thm: "real_mult_left_commute"
walther@60343	291	### try thm: "mult.assoc"
walther@60343	292	### try thm: "add.commute"
walther@60343	293	#### eval asms: "- 6 +
walther@60343	294	(- 5 * x +
walther@60343	295	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3)))) =
walther@60343	296	- 5 * x +
walther@60343	297	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3))) +
walther@60343	298	- 6"
walther@60343	299	### not >: "- 6 +
walther@60343	300	(- 5 * x +
walther@60343	301	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3))))" > "- 5 * x +
walther@60343	302	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3))) +
walther@60343	303	- 6"
walther@60343	304	#### eval asms: "- 5 * x +
walther@60343	305	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3))) =
walther@60343	306	- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3)) +
walther@60343	307	- 5 * x"
walther@60343	308	### not >: "- 5 * x +
walther@60343	309	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3)))" > "- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3)) +
walther@60343	310	- 5 * x"
walther@60343	311	#### eval asms: "- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3)) =
walther@60343	312	- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3) + - 1 * x \<up> 2"
walther@60343	313	### not >: "- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3))" > "- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3) + - 1 * x \<up> 2"
walther@60343	314	#### eval asms: "- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3) =
walther@60343	315	- 1 * x \<up> 3 + x \<up> 3 + - 14 * x \<up> 2"
walther@60343	316	### not >: "- 14 * x \<up> 2 + (- 1 * x \<up> 3 + x \<up> 3)" > "- 1 * x \<up> 3 + x \<up> 3 + - 14 * x \<up> 2"
walther@60343	317	#### eval asms: "- 1 * x \<up> 3 + x \<up> 3 = x \<up> 3 + - 1 * x \<up> 3"
walther@60343	318	### rewrites to: "- 6 + (- 5 * x + (- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3))))"
walther@60343	319	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
walther@60343	320	### try thm: "add.commute"
walther@60343	321	#### eval asms: "- 6 +
walther@60343	322	(- 5 * x +
walther@60343	323	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3)))) =
walther@60343	324	- 5 * x +
walther@60343	325	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3))) +
walther@60343	326	- 6"
walther@60343	327	### not >: "- 6 +
walther@60343	328	(- 5 * x +
walther@60343	329	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3))))" > "- 5 * x +
walther@60343	330	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3))) +
walther@60343	331	- 6"
walther@60343	332	#### eval asms: "- 5 * x +
walther@60343	333	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3))) =
walther@60343	334	- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3)) +
walther@60343	335	- 5 * x"
walther@60343	336	### not >: "- 5 * x +
walther@60343	337	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3)))" > "- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3)) +
walther@60343	338	- 5 * x"
walther@60343	339	#### eval asms: "- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3)) =
walther@60343	340	- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3) + - 1 * x \<up> 2"
walther@60343	341	### not >: "- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3))" > "- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3) + - 1 * x \<up> 2"
walther@60343	342	#### eval asms: "- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3) =
walther@60343	343	x \<up> 3 + - 1 * x \<up> 3 + - 14 * x \<up> 2"
walther@60343	344	### not >: "- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3)" > "x \<up> 3 + - 1 * x \<up> 3 + - 14 * x \<up> 2"
walther@60343	345	#### eval asms: "x \<up> 3 + - 1 * x \<up> 3 = - 1 * x \<up> 3 + x \<up> 3"
walther@60343	346	### not >: "x \<up> 3 + - 1 * x \<up> 3" > "- 1 * x \<up> 3 + x \<up> 3"
walther@60343	347	### try thm: "add.left_commute"
walther@60343	348	#### eval asms: "- 6 +
walther@60343	349	(- 5 * x +
walther@60343	350	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3)))) =
walther@60343	351	- 5 * x +
walther@60343	352	(- 6 +
walther@60343	353	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3))))"
walther@60343	354	### not >: "- 6 +
walther@60343	355	(- 5 * x +
walther@60343	356	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3))))" > "- 5 * x +
walther@60343	357	(- 6 +
walther@60343	358	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3))))"
walther@60343	359	#### eval asms: "- 5 * x +
walther@60343	360	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3))) =
walther@60343	361	- 1 * x \<up> 2 +
walther@60343	362	(- 5 * x + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3)))"
walther@60343	363	### not >: "- 5 * x +
walther@60343	364	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3)))" > "- 1 * x \<up> 2 +
walther@60343	365	(- 5 * x + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3)))"
walther@60343	366	#### eval asms: "- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3)) =
walther@60343	367	- 14 * x \<up> 2 + (- 1 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3))"
walther@60343	368	### not >: "- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3))" > "- 14 * x \<up> 2 + (- 1 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3))"
walther@60343	369	#### eval asms: "- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3) =
walther@60343	370	x \<up> 3 + (- 14 * x \<up> 2 + - 1 * x \<up> 3)"
walther@60343	371	### not >: "- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3)" > "x \<up> 3 + (- 14 * x \<up> 2 + - 1 * x \<up> 3)"
walther@60343	372	### try thm: "add.assoc"
walther@60343	373	### try thm: "mult.commute"
walther@60343	374	#### eval asms: "- 1 * x \<up> 3 = x \<up> 3 * - 1"
walther@60343	375	### not >: "- 1 * x \<up> 3" > "x \<up> 3 * - 1"
walther@60343	376	#### eval asms: "- 14 * x \<up> 2 = x \<up> 2 * - 14"
walther@60343	377	### not >: "- 14 * x \<up> 2" > "x \<up> 2 * - 14"
walther@60343	378	#### eval asms: "- 1 * x \<up> 2 = x \<up> 2 * - 1"
walther@60343	379	### not >: "- 1 * x \<up> 2" > "x \<up> 2 * - 1"
walther@60343	380	#### eval asms: "- 5 * x = x * - 5"
walther@60343	381	### not >: "- 5 * x" > "x * - 5"
walther@60343	382	### try thm: "real_mult_left_commute"
walther@60343	383	### try thm: "mult.assoc"
walther@60343	384	### try thm: "add.commute"
walther@60343	385	#### eval asms: "- 6 +
walther@60343	386	(- 5 * x +
walther@60343	387	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3)))) =
walther@60343	388	- 5 * x +
walther@60343	389	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3))) +
walther@60343	390	- 6"
walther@60343	391	### not >: "- 6 +
walther@60343	392	(- 5 * x +
walther@60343	393	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3))))" > "- 5 * x +
walther@60343	394	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3))) +
walther@60343	395	- 6"
walther@60343	396	#### eval asms: "- 5 * x +
walther@60343	397	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3))) =
walther@60343	398	- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3)) +
walther@60343	399	- 5 * x"
walther@60343	400	### not >: "- 5 * x +
walther@60343	401	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3)))" > "- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3)) +
walther@60343	402	- 5 * x"
walther@60343	403	#### eval asms: "- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3)) =
walther@60343	404	- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3) + - 1 * x \<up> 2"
walther@60343	405	### not >: "- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3))" > "- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3) + - 1 * x \<up> 2"
walther@60343	406	#### eval asms: "- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3) =
walther@60343	407	x \<up> 3 + - 1 * x \<up> 3 + - 14 * x \<up> 2"
walther@60343	408	### not >: "- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3)" > "x \<up> 3 + - 1 * x \<up> 3 + - 14 * x \<up> 2"
walther@60343	409	#### eval asms: "x \<up> 3 + - 1 * x \<up> 3 = - 1 * x \<up> 3 + x \<up> 3"
walther@60343	410	### not >: "x \<up> 3 + - 1 * x \<up> 3" > "- 1 * x \<up> 3 + x \<up> 3"
walther@60343	411	### try thm: "add.left_commute"
walther@60343	412	#### eval asms: "- 6 +
walther@60343	413	(- 5 * x +
walther@60343	414	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3)))) =
walther@60343	415	- 5 * x +
walther@60343	416	(- 6 +
walther@60343	417	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3))))"
walther@60343	418	### not >: "- 6 +
walther@60343	419	(- 5 * x +
walther@60343	420	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3))))" > "- 5 * x +
walther@60343	421	(- 6 +
walther@60343	422	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3))))"
walther@60343	423	#### eval asms: "- 5 * x +
walther@60343	424	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3))) =
walther@60343	425	- 1 * x \<up> 2 +
walther@60343	426	(- 5 * x + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3)))"
walther@60343	427	### not >: "- 5 * x +
walther@60343	428	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3)))" > "- 1 * x \<up> 2 +
walther@60343	429	(- 5 * x + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3)))"
walther@60343	430	#### eval asms: "- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3)) =
walther@60343	431	- 14 * x \<up> 2 + (- 1 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3))"
walther@60343	432	### not >: "- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3))" > "- 14 * x \<up> 2 + (- 1 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3))"
walther@60343	433	#### eval asms: "- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3) =
walther@60343	434	x \<up> 3 + (- 14 * x \<up> 2 + - 1 * x \<up> 3)"
walther@60343	435	### not >: "- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3)" > "x \<up> 3 + (- 14 * x \<up> 2 + - 1 * x \<up> 3)"
walther@60343	436	### try thm: "add.assoc"
walther@60343	437	## rls: simplify_power on: - 6 +
walther@60343	438	(- 5 * x +
walther@60343	439	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3))))
walther@60343	440	### try thm: "realpow_multI"
walther@60343	441	### try thm: "sym_realpow_twoI"
walther@60343	442	### try thm: "realpow_plus_1"
walther@60343	443	### try thm: "realpow_pow"
walther@60343	444	### try thm: "sym_realpow_addI"
walther@60343	445	### try thm: "realpow_oneI"
walther@60343	446	### try thm: "realpow_eq_oneI"
walther@60343	447	## rls: collect_numerals on: - 6 +
walther@60343	448	(- 5 * x +
walther@60343	449	(- 1 * x \<up> 2 + (- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3))))
walther@60343	450	### try thm: "real_num_collect"
walther@60343	451	### try thm: "real_num_collect_assoc"
walther@60343	452	#### eval asms: "\<lbrakk>- 1 is_const; - 14 is_const\<rbrakk>
walther@60343	453	\<Longrightarrow> - 1 * x \<up> 2 +
walther@60343	454	(- 14 * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3)) =
walther@60343	455	(- 1 + - 14) * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3)"
walther@60343	456	##### rls: Atools_erls on: - 14 is_const
walther@60343	457	###### try calc: "HOL.eq"
walther@60343	458	###### try thm: "not_true"
walther@60343	459	###### try thm: "not_false"
walther@60343	460	###### try thm: "and_true"
walther@60343	461	###### try thm: "and_false"
walther@60343	462	###### try thm: "or_true"
walther@60343	463	###### try thm: "or_false"
walther@60343	464	###### try thm: "rat_leq1"
walther@60343	465	###### try thm: "rat_leq2"
walther@60343	466	###### try thm: "rat_leq3"
walther@60343	467	###### try thm: "refl"
walther@60343	468	###### try thm: "order_refl"
walther@60343	469	###### try thm: "radd_left_cancel_le"
walther@60343	470	###### try calc: "Orderings.ord_class.less"
walther@60343	471	###### try calc: "Orderings.ord_class.less_eq"
walther@60343	472	###### try calc: "Prog_Expr.ident"
walther@60343	473	###### try calc: "Prog_Expr.is_const"
walther@60343	474	####### eval asms: "(- 14 is_const) = True"
walther@60343	475	###### calc. to: True
walther@60343	476	###### try calc: "Prog_Expr.is_const"
walther@60343	477	###### try calc: "Prog_Expr.occurs_in"
walther@60343	478	###### try calc: "Prog_Expr.matches"
walther@60343	479	###### try calc: "HOL.eq"
walther@60343	480	###### try thm: "not_true"
walther@60343	481	###### try thm: "not_false"
walther@60343	482	###### try thm: "and_true"
walther@60343	483	###### try thm: "and_false"
walther@60343	484	###### try thm: "or_true"
walther@60343	485	###### try thm: "or_false"
walther@60343	486	###### try thm: "rat_leq1"
walther@60343	487	###### try thm: "rat_leq2"
walther@60343	488	###### try thm: "rat_leq3"
walther@60343	489	###### try thm: "refl"
walther@60343	490	###### try thm: "order_refl"
walther@60343	491	###### try thm: "radd_left_cancel_le"
walther@60343	492	###### try calc: "Orderings.ord_class.less"
walther@60343	493	###### try calc: "Orderings.ord_class.less_eq"
walther@60343	494	###### try calc: "Prog_Expr.ident"
walther@60343	495	###### try calc: "Prog_Expr.is_const"
walther@60343	496	###### try calc: "Prog_Expr.occurs_in"
walther@60343	497	###### try calc: "Prog_Expr.matches"
walther@60343	498	##### rls: Atools_erls on: - 1 is_const
walther@60343	499	###### try calc: "HOL.eq"
walther@60343	500	###### try thm: "not_true"
walther@60343	501	###### try thm: "not_false"
walther@60343	502	###### try thm: "and_true"
walther@60343	503	###### try thm: "and_false"
walther@60343	504	###### try thm: "or_true"
walther@60343	505	###### try thm: "or_false"
walther@60343	506	###### try thm: "rat_leq1"
walther@60343	507	###### try thm: "rat_leq2"
walther@60343	508	###### try thm: "rat_leq3"
walther@60343	509	###### try thm: "refl"
walther@60343	510	###### try thm: "order_refl"
walther@60343	511	###### try thm: "radd_left_cancel_le"
walther@60343	512	###### try calc: "Orderings.ord_class.less"
walther@60343	513	###### try calc: "Orderings.ord_class.less_eq"
walther@60343	514	###### try calc: "Prog_Expr.ident"
walther@60343	515	###### try calc: "Prog_Expr.is_const"
walther@60343	516	####### eval asms: "(- 1 is_const) = True"
walther@60343	517	###### calc. to: True
walther@60343	518	###### try calc: "Prog_Expr.is_const"
walther@60343	519	###### try calc: "Prog_Expr.occurs_in"
walther@60343	520	###### try calc: "Prog_Expr.matches"
walther@60343	521	###### try calc: "HOL.eq"
walther@60343	522	###### try thm: "not_true"
walther@60343	523	###### try thm: "not_false"
walther@60343	524	###### try thm: "and_true"
walther@60343	525	###### try thm: "and_false"
walther@60343	526	###### try thm: "or_true"
walther@60343	527	###### try thm: "or_false"
walther@60343	528	###### try thm: "rat_leq1"
walther@60343	529	###### try thm: "rat_leq2"
walther@60343	530	###### try thm: "rat_leq3"
walther@60343	531	###### try thm: "refl"
walther@60343	532	###### try thm: "order_refl"
walther@60343	533	###### try thm: "radd_left_cancel_le"
walther@60343	534	###### try calc: "Orderings.ord_class.less"
walther@60343	535	###### try calc: "Orderings.ord_class.less_eq"
walther@60343	536	###### try calc: "Prog_Expr.ident"
walther@60343	537	###### try calc: "Prog_Expr.is_const"
walther@60343	538	###### try calc: "Prog_Expr.occurs_in"
walther@60343	539	###### try calc: "Prog_Expr.matches"
walther@60343	540	#### asms accepted: [- 14 is_const, - 1 is_const] stored: []
walther@60343	541	### rewrites to: "- 6 + (- 5 * x + ((- 1 + - 14) * x \<up> 2 + (x \<up> 3 + - 1 * x \<up> 3)))"
walther@60343	542	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
walther@60343	543	### try thm: "real_num_collect_assoc"
walther@60343	544	### try thm: "real_one_collect"
walther@60343	545	#### eval asms: "- 1 is_const \<Longrightarrow>
walther@60343	546	x \<up> 3 + - 1 * x \<up> 3 = (1 + - 1) * x \<up> 3"
walther@60343	547	##### rls: Atools_erls on: - 1 is_const
walther@60343	548	###### try calc: "HOL.eq"
walther@60343	549	###### try thm: "not_true"
walther@60343	550	###### try thm: "not_false"
walther@60343	551	###### try thm: "and_true"
walther@60343	552	###### try thm: "and_false"
walther@60343	553	###### try thm: "or_true"
walther@60343	554	###### try thm: "or_false"
walther@60343	555	###### try thm: "rat_leq1"
walther@60343	556	###### try thm: "rat_leq2"
walther@60343	557	###### try thm: "rat_leq3"
walther@60343	558	###### try thm: "refl"
walther@60343	559	###### try thm: "order_refl"
walther@60343	560	###### try thm: "radd_left_cancel_le"
walther@60343	561	###### try calc: "Orderings.ord_class.less"
walther@60343	562	###### try calc: "Orderings.ord_class.less_eq"
walther@60343	563	###### try calc: "Prog_Expr.ident"
walther@60343	564	###### try calc: "Prog_Expr.is_const"
walther@60343	565	####### eval asms: "(- 1 is_const) = True"
walther@60343	566	###### calc. to: True
walther@60343	567	###### try calc: "Prog_Expr.is_const"
walther@60343	568	###### try calc: "Prog_Expr.occurs_in"
walther@60343	569	###### try calc: "Prog_Expr.matches"
walther@60343	570	###### try calc: "HOL.eq"
walther@60343	571	###### try thm: "not_true"
walther@60343	572	###### try thm: "not_false"
walther@60343	573	###### try thm: "and_true"
walther@60343	574	###### try thm: "and_false"
walther@60343	575	###### try thm: "or_true"
walther@60343	576	###### try thm: "or_false"
walther@60343	577	###### try thm: "rat_leq1"
walther@60343	578	###### try thm: "rat_leq2"
walther@60343	579	###### try thm: "rat_leq3"
walther@60343	580	###### try thm: "refl"
walther@60343	581	###### try thm: "order_refl"
walther@60343	582	###### try thm: "radd_left_cancel_le"
walther@60343	583	###### try calc: "Orderings.ord_class.less"
walther@60343	584	###### try calc: "Orderings.ord_class.less_eq"
walther@60343	585	###### try calc: "Prog_Expr.ident"
walther@60343	586	###### try calc: "Prog_Expr.is_const"
walther@60343	587	###### try calc: "Prog_Expr.occurs_in"
walther@60343	588	###### try calc: "Prog_Expr.matches"
walther@60343	589	#### asms accepted: [- 1 is_const] stored: []
walther@60343	590	### rewrites to: "- 6 + (- 5 * x + ((- 1 + - 14) * x \<up> 2 + (1 + - 1) * x \<up> 3))"
walther@60343	591	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
walther@60343	592	### try thm: "real_one_collect"
walther@60343	593	### try thm: "real_one_collect_assoc"
walther@60343	594	### try calc: "Groups.plus_class.plus"
walther@60343	595	#### eval asms: "- 1 + - 14 = - 15"
walther@60343	596	### calc. to: - 6 + (- 5 * x + (- 15 * x \<up> 2 + (1 + - 1) * x \<up> 3))
walther@60343	597	### try calc: "Groups.plus_class.plus"
walther@60343	598	#### eval asms: "1 + - 1 = 0"
walther@60343	599	### calc. to: - 6 + (- 5 * x + (- 15 * x \<up> 2 + 0 * x \<up> 3))
walther@60343	600	### try calc: "Groups.plus_class.plus"
walther@60343	601	### try calc: "Groups.times_class.times"
walther@60343	602	### try calc: "Transcendental.powr"
walther@60343	603	### try thm: "real_num_collect"
walther@60343	604	### try thm: "real_num_collect_assoc"
walther@60343	605	### try thm: "real_one_collect"
walther@60343	606	### try thm: "real_one_collect_assoc"
walther@60343	607	### try calc: "Groups.plus_class.plus"
walther@60343	608	### try calc: "Groups.times_class.times"
walther@60343	609	### try calc: "Transcendental.powr"
walther@60343	610	## rls: reduce_012 on: - 6 + (- 5 * x + (- 15 * x \<up> 2 + 0 * x \<up> 3))
walther@60343	611	^^^^^^^^^^^^^^^^^^#####^^^^^^^^^^^^^^^^^^^^^
walther@60343	612	### try thm: "mult_1_left"
walther@60343	613	### try thm: "minus_mult_left" <<<<<----------------------------------------------
walther@60343	614	#### eval asms: "- 15 * x \<up> 2 = - (15 * x \<up> 2)"
walther@60343	615	### rewrites to: "- 6 + (- 5 * x + (- (15 * x \<up> 2) + 0 * x \<up> 3))"
walther@60343	616	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^####^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
walther@60343	617	### try thm: "minus_mult_left" <<<<<----------------------------------------------
walther@60343	618	#### eval asms: "- 5 * x = - (5 * x)"
walther@60343	619	### rewrites to: "- 6 + (- (5 * x) + (- (15 * x \<up> 2) + 0 * x \<up> 3))"
walther@60343	620	^^^^^^^^^^^^^^^^^^^^####^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
walther@60343	621	### try thm: "minus_mult_left"
walther@60343	622	### try thm: "mult_zero_left"
walther@60343	623	#### eval asms: "0 * x \<up> 3 = 0"
walther@60343	624	### rewrites to: "- 6 + (- (5 * x) + (- (15 * x \<up> 2) + 0))"
walther@60343	625	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
walther@60343	626	### try thm: "mult_zero_left"
walther@60343	627	### try thm: "add_0_left"
walther@60343	628	### try thm: "right_minus"
walther@60343	629	### try thm: "sym_real_mult_2"
walther@60343	630	### try thm: "real_mult_2_assoc"
walther@60343	631	### try thm: "mult_1_left"
walther@60343	632	### try thm: "minus_mult_left"
walther@60343	633	### try thm: "mult_zero_left"
walther@60343	634	### try thm: "add_0_left"
walther@60343	635	### try thm: "right_minus"
walther@60343	636	### try thm: "sym_real_mult_2"
walther@60343	637	### try thm: "real_mult_2_assoc"
walther@60343	638	## try thm: "realpow_oneI"
walther@60343	639	## rls: discard_parentheses on: - 6 + (- (5 * x) + (- (15 * x \<up> 2) + 0))
walther@60343	640	### try thm: "sym_mult.assoc"
walther@60343	641	### try thm: "sym_add.assoc"
walther@60343	642	#### eval asms: "- 6 + (- (5 * x) + (- (15 * x \<up> 2) + 0)) =
walther@60343	643	- 6 + - (5 * x) + (- (15 * x \<up> 2) + 0)"
walther@60343	644	### rewrites to: "- 6 + - (5 * x) + (- (15 * x \<up> 2) + 0)"
walther@60343	645	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
walther@60343	646	### try thm: "sym_add.assoc"
walther@60343	647	#### eval asms: "- 6 + - (5 * x) + (- (15 * x \<up> 2) + 0) =
walther@60343	648	- 6 + - (5 * x) + - (15 * x \<up> 2) + 0"
walther@60343	649	### rewrites to: "- 6 + - (5 * x) + - (15 * x \<up> 2) + 0"
walther@60343	650	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
walther@60343	651	### try thm: "sym_add.assoc"
walther@60343	652	### try thm: "sym_mult.assoc"
walther@60343	653	### try thm: "sym_add.assoc"
walther@60343	654	## rls: collect_bdv on: - 6 + - (5 * x) + - (15 * x \<up> 2) + 0
walther@60343	655	### try thm: "bdv_collect_1"
walther@60343	656	### try thm: "bdv_collect_2"
walther@60343	657	### try thm: "bdv_collect_3"
walther@60343	658	### try thm: "bdv_collect_assoc1_1"
walther@60343	659	### try thm: "bdv_collect_assoc1_2"
walther@60343	660	### try thm: "bdv_collect_assoc1_3"
walther@60343	661	### try thm: "bdv_collect_assoc2_1"
walther@60343	662	### try thm: "bdv_collect_assoc2_2"
walther@60343	663	### try thm: "bdv_collect_assoc2_3"
walther@60343	664	### try thm: "bdv_n_collect_1"
walther@60343	665	### try thm: "bdv_n_collect_2"
walther@60343	666	### try thm: "bdv_n_collect_3"
walther@60343	667	### try thm: "bdv_n_collect_assoc1_1"
walther@60343	668	### try thm: "bdv_n_collect_assoc1_2"
walther@60343	669	### try thm: "bdv_n_collect_assoc1_3"
walther@60343	670	### try thm: "bdv_n_collect_assoc2_1"
walther@60343	671	### try thm: "bdv_n_collect_assoc2_2"
walther@60343	672	### try thm: "bdv_n_collect_assoc2_3"
walther@60343	673	val t' =
walther@60343	674	Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $
walther@60343	675	(Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $
walther@60343	676	(Const ("Groups.plus_class.plus", "real \<Rightarrow> real \<Rightarrow> real") $
walther@60343	677	(Const ("Groups.uminus_class.uminus", "real \<Rightarrow> real") $
walther@60343	678	(Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $ (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ (Const ("Num.num.Bit1", "num \<Rightarrow> num") $ Const ("Num.num.One", "num"))))) $
walther@60343	679	(Const ("Groups.uminus_class.uminus", "real \<Rightarrow> real") $
walther@60343	680	(Const ("Groups.times_class.times", "real \<Rightarrow> real \<Rightarrow> real") $
walther@60343	681	(Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $ (Const ("Num.num.Bit1", "num \<Rightarrow> num") $ (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num")))) $ Free ("x", "real")))) $
walther@60343	682	(Const ("Groups.uminus_class.uminus", "real \<Rightarrow> real") $
walther@60343	683	(Const ("Groups.times_class.times", "real \<Rightarrow> real \<Rightarrow> real") $
walther@60343	684	(Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $
walther@60343	685	(Const ("Num.num.Bit1", "num \<Rightarrow> num") $ (Const ("Num.num.Bit1", "num \<Rightarrow> num") $ (Const ("Num.num.Bit1", "num \<Rightarrow> num") $ Const ("Num.num.One", "num"))))) $
walther@60343	686	(Const ("Transcendental.powr", "real \<Rightarrow> real \<Rightarrow> real") $ Free ("x", "real") $
walther@60343	687	(Const ("Num.numeral_class.numeral", "num \<Rightarrow> real") $ (Const ("Num.num.Bit0", "num \<Rightarrow> num") $ Const ("Num.num.One", "num"))))))) $
walther@60343	688	Const ("Groups.zero_class.zero", "real"):
walther@60343	689	term

author	wneuper <walther.neuper@jku.at>
	Mon, 02 Aug 2021 11:38:40 +0200
changeset 60343	f6e98785473f
permissions	-rw-r--r--