517 moreover have "th' \<noteq> th" using neq_th' . |
518 moreover have "th' \<noteq> th" using neq_th' . |
518 ultimately show ?thesis by simp |
519 ultimately show ?thesis by simp |
519 qed |
520 qed |
520 qed |
521 qed |
521 |
522 |
522 lemmas eq_pv_blocked_dtc = eq_pv_blocked[folded detached_eq] |
523 text {* |
523 |
524 The following lemma is the extrapolation of @{thm eq_pv_blocked}. |
524 |
525 It says if a thread, different from @{term th}, |
525 |
526 does not hold any resource at the very beginning, |
526 lemma eq_pv_kept: (* ddd *) |
527 it will keep hand-emptied in the future @{term "t@s"}. |
527 assumes th'_in: "th' \<in> threads s" |
528 *} |
|
529 lemma eq_pv_persist: (* ddd *) |
|
530 assumes neq_th': "th' \<noteq> th" |
528 and eq_pv: "cntP s th' = cntV s th'" |
531 and eq_pv: "cntP s th' = cntV s th'" |
529 and neq_th': "th' \<noteq> th" |
532 shows "cntP (t@s) th' = cntV (t@s) th'" |
530 shows "th' \<in> threads (t@s) \<and> |
533 proof(induction rule:ind) -- {* The proof goes by induction. *} |
531 cntP (t@s) th' = cntV (t@s) th'" |
534 -- {* The nontrivial case is for the @{term Cons}: *} |
532 proof(induct rule:ind) |
|
533 case (Cons e t) |
535 case (Cons e t) |
534 interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp |
536 -- {* All results derived so far hold for both @{term s} and @{term "t@s"}: *} |
535 interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp |
537 interpret vat_t: extend_highest_gen s th prio tm t using Cons by simp |
536 show ?case |
538 interpret vat_e: extend_highest_gen s th prio tm "(e # t)" using Cons by simp |
537 proof(cases e) |
539 show ?case |
538 case (P thread cs) |
540 proof - |
539 show ?thesis |
541 -- {* It can be proved that @{term cntP}-value of @{term th'} does not change |
540 proof - |
542 by the happening of event @{term e}: *} |
541 have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" |
543 have "cntP ((e#t)@s) th' = cntP (t@s) th'" |
542 proof - |
544 proof(rule ccontr) -- {* Proof by contradiction. *} |
543 have "thread \<noteq> th'" |
545 -- {* Suppose @{term cntP}-value of @{term th'} is changed by @{term e}: *} |
544 proof - |
546 assume otherwise: "cntP ((e # t) @ s) th' \<noteq> cntP (t @ s) th'" |
545 have "step (t@s) (P thread cs)" using Cons P by auto |
547 -- {* Then the actor of @{term e} must be @{term th'} and @{term e} |
546 thus ?thesis |
548 must be a @{term P}-event: *} |
547 proof(cases) |
549 hence "isP e" "actor e = th'" by (auto simp:cntP_diff_inv) |
548 assume "thread \<in> runing (t@s)" |
550 with vat_t.actor_inv[OF Cons(2)] |
549 moreover have "th' \<notin> runing (t@s)" using Cons(5) |
551 -- {* According to @{thm actor_inv}, @{term th'} must be running at |
550 by (metis neq_th' vat_t.eq_pv_blocked) |
552 the moment @{term "t@s"}: *} |
551 ultimately show ?thesis by auto |
553 have "th' \<in> runing (t@s)" by (cases e, auto) |
552 qed |
554 -- {* However, an application of @{thm eq_pv_blocked} to induction hypothesis |
553 qed with Cons show ?thesis |
555 shows @{term th'} can not be running at moment @{term "t@s"}: *} |
554 by (unfold P, simp add:cntP_def cntV_def count_def) |
556 moreover have "th' \<notin> runing (t@s)" |
555 qed |
557 using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] . |
556 moreover have "th' \<in> threads ((e # t) @ s)" using Cons by (unfold P, simp) |
558 -- {* Contradiction is finally derived: *} |
557 ultimately show ?thesis by auto |
559 ultimately show False by simp |
558 qed |
|
559 next |
|
560 case (V thread cs) |
|
561 show ?thesis |
|
562 proof - |
|
563 have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" |
|
564 proof - |
|
565 have "thread \<noteq> th'" |
|
566 proof - |
|
567 have "step (t@s) (V thread cs)" using Cons V by auto |
|
568 thus ?thesis |
|
569 proof(cases) |
|
570 assume "thread \<in> runing (t@s)" |
|
571 moreover have "th' \<notin> runing (t@s)" using Cons(5) |
|
572 by (metis neq_th' vat_t.eq_pv_blocked) |
|
573 ultimately show ?thesis by auto |
|
574 qed |
|
575 qed with Cons show ?thesis |
|
576 by (unfold V, simp add:cntP_def cntV_def count_def) |
|
577 qed |
|
578 moreover have "th' \<in> threads ((e # t) @ s)" using Cons by (unfold V, simp) |
|
579 ultimately show ?thesis by auto |
|
580 qed |
|
581 next |
|
582 case (Create thread prio') |
|
583 show ?thesis |
|
584 proof - |
|
585 have "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" |
|
586 proof - |
|
587 have "thread \<noteq> th'" |
|
588 proof - |
|
589 have "step (t@s) (Create thread prio')" using Cons Create by auto |
|
590 thus ?thesis using Cons(5) by (cases, auto) |
|
591 qed with Cons show ?thesis |
|
592 by (unfold Create, simp add:cntP_def cntV_def count_def) |
|
593 qed |
|
594 moreover have "th' \<in> threads ((e # t) @ s)" using Cons by (unfold Create, simp) |
|
595 ultimately show ?thesis by auto |
|
596 qed |
|
597 next |
|
598 case (Exit thread) |
|
599 show ?thesis |
|
600 proof - |
|
601 have neq_thread: "thread \<noteq> th'" |
|
602 proof - |
|
603 have "step (t@s) (Exit thread)" using Cons Exit by auto |
|
604 thus ?thesis apply (cases) using Cons(5) |
|
605 by (metis neq_th' vat_t.eq_pv_blocked) |
|
606 qed |
|
607 hence "cntP ((e # t) @ s) th' = cntV ((e # t) @ s) th'" using Cons |
|
608 by (unfold Exit, simp add:cntP_def cntV_def count_def) |
|
609 moreover have "th' \<in> threads ((e # t) @ s)" using Cons neq_thread |
|
610 by (unfold Exit, simp) |
|
611 ultimately show ?thesis by auto |
|
612 qed |
|
613 next |
|
614 case (Set thread prio') |
|
615 with Cons |
|
616 show ?thesis |
|
617 by (auto simp:cntP_def cntV_def count_def) |
|
618 qed |
560 qed |
619 next |
561 -- {* It can also be proved that @{term cntV}-value of @{term th'} does not change |
620 case Nil |
562 by the happening of event @{term e}: *} |
621 with assms |
563 -- {* The proof follows exactly the same pattern as the case for @{term cntP}-value: *} |
622 show ?case by auto |
564 moreover have "cntV ((e#t)@s) th' = cntV (t@s) th'" |
623 qed |
565 proof(rule ccontr) -- {* Proof by contradiction. *} |
624 |
566 assume otherwise: "cntV ((e # t) @ s) th' \<noteq> cntV (t @ s) th'" |
625 (* runing_precond has changed to eq_pv_kept *) |
567 hence "isV e" "actor e = th'" by (auto simp:cntV_diff_inv) |
626 |
568 with vat_t.actor_inv[OF Cons(2)] |
627 text {* Changing counting balance to detachedness *} |
569 have "th' \<in> runing (t@s)" by (cases e, auto) |
628 lemmas eq_pv_kept_dtc = eq_pv_kept |
570 moreover have "th' \<notin> runing (t@s)" |
629 [folded vat_t.detached_eq vat_s.detached_eq] |
571 using vat_t.eq_pv_blocked[OF neq_th' Cons(5)] . |
630 |
572 ultimately show False by simp |
631 section {* The blocking thread *} |
573 qed |
|
574 -- {* Finally, it can be shown that the @{term cntP} and @{term cntV} |
|
575 value for @{term th'} are still in balance, so @{term th'} |
|
576 is still hand-emptied after the execution of event @{term e}: *} |
|
577 ultimately show ?thesis using Cons(5) by metis |
|
578 qed |
|
579 qed (auto simp:eq_pv) |
|
580 |
|
581 text {* |
|
582 By combining @{thm eq_pv_blocked} and @{thm eq_pv_persist}, |
|
583 it can be derived easily that @{term th'} can not be running in the future: |
|
584 *} |
|
585 lemma eq_pv_blocked_persist: |
|
586 assumes neq_th': "th' \<noteq> th" |
|
587 and eq_pv: "cntP s th' = cntV s th'" |
|
588 shows "th' \<notin> runing (t@s)" |
|
589 using assms |
|
590 by (simp add: eq_pv_blocked eq_pv_persist) |
632 |
591 |
633 text {* |
592 text {* |
634 The purpose of PIP is to ensure that the most |
593 The purpose of PIP is to ensure that the most |
635 urgent thread @{term th} is not blocked unreasonably. |
594 urgent thread @{term th} is not blocked unreasonably. |
636 Therefore, a clear picture of the blocking thread is essential |
595 Therefore, a clear picture of the blocking thread is essential |
637 to assure people that the purpose is fulfilled. |
596 to assure people that the purpose is fulfilled. |
638 |
597 |
639 The following lemmas will give us such a picture: |
598 The following lemmas will give us such a picture: |
640 *} |
599 *} |
641 |
600 |
642 (* ccc *) |
|
643 |
|
644 text {* |
601 text {* |
645 The following lemma shows the blocking thread @{term th'} |
602 The following lemma shows the blocking thread @{term th'} |
646 must hold some resource in the very beginning. |
603 must hold some resource in the very beginning. |
647 *} |
604 *} |
648 lemma runing_cntP_cntV_inv: (* ddd *) |
605 lemma runing_cntP_cntV_inv: (* ddd *) |
649 assumes th'_in: "th' \<in> threads s" |
606 assumes is_runing: "th' \<in> runing (t@s)" |
650 and neq_th': "th' \<noteq> th" |
607 and neq_th': "th' \<noteq> th" |
651 and is_runing: "th' \<in> runing (t@s)" |
|
652 shows "cntP s th' > cntV s th'" |
608 shows "cntP s th' > cntV s th'" |
653 using assms |
609 using assms |
654 proof - (* ccc *) |
610 proof - |
655 -- {* First, it can be shown that the number of @{term P} and |
611 -- {* First, it can be shown that the number of @{term P} and |
656 @{term V} operations can not be equal for thred @{term th'} *} |
612 @{term V} operations can not be equal for thred @{term th'} *} |
657 have "cntP s th' \<noteq> cntV s th'" |
613 have "cntP s th' \<noteq> cntV s th'" |
658 proof |
614 proof |
|
615 -- {* The proof goes by contradiction, suppose otherwise: *} |
659 assume otherwise: "cntP s th' = cntV s th'" |
616 assume otherwise: "cntP s th' = cntV s th'" |
660 -- {* The proof goes by contradiction. *} |
617 -- {* By applying @{thm eq_pv_blocked_persist} to this: *} |
661 -- {* We can show that @{term th'} can not be running at moment @{term "t@s"}: *} |
618 from eq_pv_blocked_persist[OF neq_th' otherwise] |
662 have "th' \<notin> runing (t@s)" |
619 -- {* we have that @{term th'} can not be running at moment @{term "t@s"}: *} |
663 proof(rule eq_pv_blocked) |
620 have "th' \<notin> runing (t@s)" . |
664 show "th' \<noteq> th" using neq_th' by simp |
|
665 next |
|
666 show "cntP (t @ s) th' = cntV (t @ s) th'" |
|
667 using eq_pv_kept[OF th'_in otherwise neq_th'] by simp |
|
668 qed |
|
669 -- {* This is obvious in contradiction with assumption @{thm is_runing} *} |
621 -- {* This is obvious in contradiction with assumption @{thm is_runing} *} |
670 thus False using is_runing by simp |
622 thus False using is_runing by simp |
671 qed |
623 qed |
|
624 -- {* However, the number of @{term V} is always less or equal to @{term P}: *} |
672 moreover have "cntV s th' \<le> cntP s th'" using vat_s.cnp_cnv_cncs by auto |
625 moreover have "cntV s th' \<le> cntP s th'" using vat_s.cnp_cnv_cncs by auto |
|
626 -- {* Thesis is finally derived by combining the these two results: *} |
673 ultimately show ?thesis by auto |
627 ultimately show ?thesis by auto |
674 qed |
628 qed |
675 |
629 |
676 lemma moment_blocked_pre: |
|
677 assumes neq_th': "th' \<noteq> th" |
|
678 and th'_in: "th' \<in> threads ((moment i t)@s)" |
|
679 and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'" |
|
680 shows "cntP ((moment (i+j) t)@s) th' = cntV ((moment (i+j) t)@s) th' \<and> |
|
681 th' \<in> threads ((moment (i+j) t)@s)" |
|
682 proof - |
|
683 interpret h_i: red_extend_highest_gen _ _ _ _ _ i |
|
684 by (unfold_locales) |
|
685 interpret h_j: red_extend_highest_gen _ _ _ _ _ "i+j" |
|
686 by (unfold_locales) |
|
687 interpret h: extend_highest_gen "((moment i t)@s)" th prio tm "moment j (restm i t)" |
|
688 proof(unfold_locales) |
|
689 show "vt (moment i t @ s)" by (metis h_i.vt_t) |
|
690 next |
|
691 show "th \<in> threads (moment i t @ s)" by (metis h_i.th_kept) |
|
692 next |
|
693 show "preced th (moment i t @ s) = |
|
694 Max (cp (moment i t @ s) ` threads (moment i t @ s))" |
|
695 by (metis h_i.th_cp_max h_i.th_cp_preced h_i.th_kept) |
|
696 next |
|
697 show "preced th (moment i t @ s) = Prc prio tm" by (metis h_i.th_kept preced_th) |
|
698 next |
|
699 show "vt (moment j (restm i t) @ moment i t @ s)" |
|
700 using moment_plus_split by (metis add.commute append_assoc h_j.vt_t) |
|
701 next |
|
702 fix th' prio' |
|
703 assume "Create th' prio' \<in> set (moment j (restm i t))" |
|
704 thus "prio' \<le> prio" using assms |
|
705 by (metis Un_iff add.commute h_j.create_low moment_plus_split set_append) |
|
706 next |
|
707 fix th' prio' |
|
708 assume "Set th' prio' \<in> set (moment j (restm i t))" |
|
709 thus "th' \<noteq> th \<and> prio' \<le> prio" |
|
710 by (metis Un_iff add.commute h_j.set_diff_low moment_plus_split set_append) |
|
711 next |
|
712 fix th' |
|
713 assume "Exit th' \<in> set (moment j (restm i t))" |
|
714 thus "th' \<noteq> th" |
|
715 by (metis Un_iff add.commute h_j.exit_diff moment_plus_split set_append) |
|
716 qed |
|
717 show ?thesis |
|
718 by (metis add.commute append_assoc eq_pv h.eq_pv_kept |
|
719 moment_plus_split neq_th' th'_in) |
|
720 qed |
|
721 |
|
722 lemma moment_blocked_eqpv: (* ddd *) |
|
723 assumes neq_th': "th' \<noteq> th" |
|
724 and th'_in: "th' \<in> threads ((moment i t)@s)" |
|
725 and eq_pv: "cntP ((moment i t)@s) th' = cntV ((moment i t)@s) th'" |
|
726 and le_ij: "i \<le> j" |
|
727 shows "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th' \<and> |
|
728 th' \<in> threads ((moment j t)@s) \<and> |
|
729 th' \<notin> runing ((moment j t)@s)" |
|
730 proof - |
|
731 from moment_blocked_pre [OF neq_th' th'_in eq_pv, of "j-i"] and le_ij |
|
732 have h1: "cntP ((moment j t)@s) th' = cntV ((moment j t)@s) th'" |
|
733 and h2: "th' \<in> threads ((moment j t)@s)" by auto |
|
734 moreover have "th' \<notin> runing ((moment j t)@s)" |
|
735 proof - |
|
736 interpret h: red_extend_highest_gen _ _ _ _ _ j by (unfold_locales) |
|
737 show ?thesis |
|
738 using h.eq_pv_blocked h1 h2 neq_th' by auto |
|
739 qed |
|
740 ultimately show ?thesis by auto |
|
741 qed |
|
742 |
|
743 (* The foregoing two lemmas are preparation for this one, but |
|
744 in long run can be combined. Maybe I am wrong. |
|
745 This one is useless (* XY *) |
|
746 *) |
|
747 lemma moment_blocked: |
|
748 assumes neq_th': "th' \<noteq> th" |
|
749 and th'_in: "th' \<in> threads ((moment i t)@s)" |
|
750 and dtc: "detached (moment i t @ s) th'" |
|
751 and le_ij: "i \<le> j" |
|
752 shows "detached (moment j t @ s) th' \<and> |
|
753 th' \<in> threads ((moment j t)@s) \<and> |
|
754 th' \<notin> runing ((moment j t)@s)" |
|
755 proof - |
|
756 interpret h_i: red_extend_highest_gen _ _ _ _ _ i by (unfold_locales) |
|
757 interpret h_j: red_extend_highest_gen _ _ _ _ _ j by (unfold_locales) |
|
758 have cnt_i: "cntP (moment i t @ s) th' = cntV (moment i t @ s) th'" |
|
759 by (metis dtc h_i.detached_elim) |
|
760 from moment_blocked_eqpv[OF neq_th' th'_in cnt_i le_ij] |
|
761 show ?thesis by (metis h_j.detached_intro) |
|
762 qed |
|
763 |
630 |
764 text {* |
631 text {* |
765 The following lemmas shows the blocking thread @{text th'} must be live |
632 The following lemmas shows the blocking thread @{text th'} must be live |
766 at the very beginning, i.e. the moment (or state) @{term s}. |
633 at the very beginning, i.e. the moment (or state) @{term s}. |
767 *} |
634 |
768 lemma runing_threads_inv: (* ddd *) (* ccc *) |
635 The proof is a simple combination of the results above: |
|
636 *} |
|
637 lemma runing_threads_inv: |
769 assumes runing': "th' \<in> runing (t@s)" |
638 assumes runing': "th' \<in> runing (t@s)" |
770 and neq_th': "th' \<noteq> th" |
639 and neq_th': "th' \<noteq> th" |
771 shows "th' \<in> threads s" |
640 shows "th' \<in> threads s" |
772 proof - |
641 proof(rule ccontr) -- {* Proof by contradiction: *} |
773 -- {* The proof is by contradiction: *} |
642 assume otherwise: "th' \<notin> threads s" |
774 { assume otherwise: "\<not> ?thesis" |
643 have "th' \<notin> runing (t @ s)" |
775 have "th' \<notin> runing (t @ s)" |
644 proof - |
776 proof - |
645 from vat_s.cnp_cnv_eq[OF otherwise] |
777 -- {* Since @{term "th'"} is running at time @{term "t@s"}, so it exists that time. *} |
646 have "cntP s th' = cntV s th'" . |
778 have th'_in: "th' \<in> threads (t@s)" using runing' by (simp add:runing_def readys_def) |
647 from eq_pv_blocked_persist[OF neq_th' this] |
779 -- {* However, @{text "th'"} does not exist at very beginning. *} |
648 show ?thesis . |
780 have th'_notin: "th' \<notin> threads (moment 0 t @ s)" using otherwise |
649 qed |
781 by (metis append.simps(1) moment_zero) |
650 with runing' show False by simp |
782 -- {* Therefore, there must be a moment during @{text "t"}, when |
|
783 @{text "th'"} came into being. *} |
|
784 -- {* Let us suppose the moment being @{text "i"}: *} |
|
785 from p_split_gen[OF th'_in th'_notin] |
|
786 obtain i where lt_its: "i < length t" |
|
787 and le_i: "0 \<le> i" |
|
788 and pre: " th' \<notin> threads (moment i t @ s)" (is "th' \<notin> threads ?pre") |
|
789 and post: "(\<forall>i'>i. th' \<in> threads (moment i' t @ s))" by (auto) |
|
790 interpret h_i: red_extend_highest_gen _ _ _ _ _ i by (unfold_locales) |
|
791 interpret h_i': red_extend_highest_gen _ _ _ _ _ "(Suc i)" by (unfold_locales) |
|
792 from lt_its have "Suc i \<le> length t" by auto |
|
793 -- {* Let us also suppose the event which makes this change is @{text e}: *} |
|
794 from moment_head[OF this] obtain e where |
|
795 eq_me: "moment (Suc i) t = e # moment i t" by blast |
|
796 hence "vt (e # (moment i t @ s))" by (metis append_Cons h_i'.vt_t) |
|
797 hence "PIP (moment i t @ s) e" by (cases, simp) |
|
798 -- {* It can be derived that this event @{text "e"}, which |
|
799 gives birth to @{term "th'"} must be a @{term "Create"}: *} |
|
800 from create_pre[OF this, of th'] |
|
801 obtain prio where eq_e: "e = Create th' prio" |
|
802 by (metis append_Cons eq_me lessI post pre) |
|
803 have h1: "th' \<in> threads (moment (Suc i) t @ s)" using post by auto |
|
804 have h2: "cntP (moment (Suc i) t @ s) th' = cntV (moment (Suc i) t@ s) th'" |
|
805 proof - |
|
806 have "cntP (moment i t@s) th' = cntV (moment i t@s) th'" |
|
807 by (metis h_i.cnp_cnv_eq pre) |
|
808 thus ?thesis by (simp add:eq_me eq_e cntP_def cntV_def count_def) |
|
809 qed |
|
810 show ?thesis |
|
811 using moment_blocked_eqpv [OF neq_th' h1 h2, of "length t"] lt_its moment_ge |
|
812 by auto |
|
813 qed |
|
814 with `th' \<in> runing (t@s)` |
|
815 have False by simp |
|
816 } thus ?thesis by auto |
|
817 qed |
651 qed |
818 |
652 |
819 text {* |
653 text {* |
820 The following lemma summarizes several foregoing |
654 The following lemma summarizes several foregoing |
821 lemmas to give an overall picture of the blocking thread @{text "th'"}: |
655 lemmas to give an overall picture of the blocking thread @{text "th'"}: |
822 *} |
656 *} |
823 lemma runing_inversion: |
657 lemma runing_inversion: (* ddd, one of the main lemmas to present *) |
824 assumes runing': "th' \<in> runing (t@s)" |
658 assumes runing': "th' \<in> runing (t@s)" |
825 and neq_th: "th' \<noteq> th" |
659 and neq_th: "th' \<noteq> th" |
826 shows "th' \<in> threads s" |
660 shows "th' \<in> threads s" |
827 and "\<not>detached s th'" |
661 and "\<not>detached s th'" |
828 and "cp (t@s) th' = preced th s" |
662 and "cp (t@s) th' = preced th s" |
829 proof - |
663 proof - |
830 from runing_threads_inv[OF assms] |
664 from runing_threads_inv[OF assms] |
831 show "th' \<in> threads s" . |
665 show "th' \<in> threads s" . |
832 next |
666 next |
833 from runing_cntP_cntV_inv[OF runing_threads_inv[OF assms] neq_th runing'] |
667 from runing_cntP_cntV_inv[OF runing' neq_th] |
834 show "\<not>detached s th'" using vat_s.detached_eq by simp |
668 show "\<not>detached s th'" using vat_s.detached_eq by simp |
835 next |
669 next |
836 from runing_preced_inversion[OF runing'] |
670 from runing_preced_inversion[OF runing'] |
837 show "cp (t@s) th' = preced th s" . |
671 show "cp (t@s) th' = preced th s" . |
838 qed |
672 qed |
|
673 |
|
674 section {* The existence of `blocking thread` *} |
839 |
675 |
840 text {* |
676 text {* |
841 Suppose @{term th} is not running, it is first shown that |
677 Suppose @{term th} is not running, it is first shown that |
842 there is a path in RAG leading from node @{term th} to another thread @{text "th'"} |
678 there is a path in RAG leading from node @{term th} to another thread @{text "th'"} |
843 in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}). |
679 in the @{term readys}-set (So @{text "th'"} is an ancestor of @{term th}}). |