equal
deleted
inserted
replaced
616 " concatLen (STAR v) = Suc (concatLen v)" |
616 " concatLen (STAR v) = Suc (concatLen v)" |
617 |
617 |
618 text\<open>Antimirov's Theorem 3.8:\<close> |
618 text\<open>Antimirov's Theorem 3.8:\<close> |
619 lemma Maxsubterms38: |
619 lemma Maxsubterms38: |
620 shows "\<forall>pt \<in> (pders_Set UNIV t). pt \<in> (subs t) \<or> pt = ONE \<or> pt = (SEQ t0 t1)" |
620 shows "\<forall>pt \<in> (pders_Set UNIV t). pt \<in> (subs t) \<or> pt = ONE \<or> pt = (SEQ t0 t1)" |
|
621 oops |
|
622 |
621 |
623 |
622 |
624 |
623 |
625 |
624 export_code height pders subs pderso in Scala module_name Pders |
626 export_code height pders subs pderso in Scala module_name Pders |
625 export_code pdero pderso in Scala module_name Pderso |
627 export_code pdero pderso in Scala module_name Pderso |