equal
deleted
inserted
replaced
613 "concatLen (CH c) = 0" | |
613 "concatLen (CH c) = 0" | |
614 "concatLen (SEQ v1 v2) = Suc (max (concatLen v1) (concatLen v2))" | |
614 "concatLen (SEQ v1 v2) = Suc (max (concatLen v1) (concatLen v2))" | |
615 " concatLen (ALT v1 v2) = max (concatLen v1) (concatLen v2)" | |
615 " concatLen (ALT v1 v2) = max (concatLen v1) (concatLen v2)" | |
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> |
|
619 lemma Maxsubterms38: |
|
620 shows "\<forall>pt \<in> (pders_Set UNIV t). pt \<in> (subs t) \<or> pt = ONE \<or> pt = (SEQ t0 t1)" |
|
621 |
618 |
622 |
619 |
623 |
620 export_code height pders subs pderso in Scala module_name Pders |
624 export_code height pders subs pderso in Scala module_name Pders |
621 export_code pdero pderso in Scala module_name Pderso |
625 export_code pdero pderso in Scala module_name Pderso |
622 export_code pdero pderso in Scala module_name Pderso |
626 export_code pdero pderso in Scala module_name Pderso |