4 Коммуникационный протокол с таймером - устройство и обоснование корректности (1185642), страница 4
Текст из файла (страница 4)
ýòî äåéñòâèå íåâëèÿåò íà ïåðåìåííûå ýòèõ ñîîòíîøåíèé.Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Rq : { hdata, s, i, w , ρi ∈ Mq }begin receive hdata, s, i, w , ρi ;if crtheni = Exp then begin Rt := R ; Exp := i + 1 ; deliver w endelse if s = true then begin create (Rt, Exp) ; (* cr := true *)Rt := R ; Exp := i + 1 ; deliver w endifendcr ⇒ 0 < Rt ≤ R∧ ∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µ∧ hdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + R∧ cr ⇒ cs ∧ St ≥ Rt + µ(2)(4)(5)(6)Ñîîòíîøåíèå (2) ñîõðàíÿåòñÿ, ò.ê.
ïåðåìåííîé Rt âñåãäàïðèñâàèâàåòñÿ çíà÷åíèå R (åñëè ïðèñâàèâàíèå èìååò ìåñòî).Ñîîòíîøåíèå (6) ñîõðàíÿåòñÿ, ò.ê. ïåðåìåííîé Rtïðèñâàèâàåòñÿ çíà÷åíèå R òîëüêî ïðè ïîëó÷åíèè ïàêåòàhdata, s, i, w , ρi, à èç (4) è (5) ñëåäóåò, ÷òî â ýòîì ñëó÷àåâûïîëíÿåòñÿ ôîðìóëà cs ∧ St ≥ R + µ .Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Sq :(* Îòïðàâèòü ïîäòâåðæäåíèå *){ cr }begin send hack, Exp, µi endP0 ≡∧∧∧∧∧∧∧cs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Ñîîòíîøåíèÿ (1-3),(5-6) è (8) ñîõðàíÿþòñÿ, ò.ê.
ýòî äåéñòâèå íåâëèÿåò íà ïåðåìåííûå ýòèõ ñîîòíîøåíèé.(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Sq :(* Îòïðàâèòü ïîäòâåðæäåíèå *){ cr }begin send hack, Exp, µi endP0 ≡∧∧∧∧∧∧∧cs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Ñîîòíîøåíèå (4) ñîõðàíÿåòñÿ, ò.ê. ïðè îòïðàâëåíèè êàæäîãîïàêåòà îñòàâøååñÿ âðåìÿ åãî æèçíè ïîëàãàåòñÿ ðàâíûì µ .(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Sq :(* Îòïðàâèòü ïîäòâåðæäåíèå *){ cr }begin send hack, Exp, µi endP0 ≡∧∧∧∧∧∧∧cs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Ñîîòíîøåíèå (7) ñîõðàíÿåòñÿ, ò.ê.
ïðè îòïðàâëåíèè ïàêåòàhack, i, ρi â ñëó÷àå, êîãäà cr èìååò çíà÷åíèå true, âûïîëíÿåòñÿðàâåíñòâî ρ = µ , è ïîýòîìó èç ñîîòíîøåíèé (2) è (6) ñëåäóåòSt > µ .(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Loss:{m∈M }(* M ýòî ëèáî Mp , ëèáî Mq *)remove m from M endbeginP0 ≡∧∧∧∧∧∧∧cs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Ñîîòíîøåíèÿ (1-3) è (6) ñîõðàíÿþòñÿ, ò.ê.
ýòî äåéñòâèå íåâëèÿåò íà ïåðåìåííûå ýòèõ ñîîòíîøåíèé. Ñîîòíîøåíèÿ (4-5) è(7-8) ñîõðàíÿþòñÿ, ò.ê. èçúÿòèå ïàêåòà ìîæåò ïðèâåñòè ëèøü êòîìó, ÷òî íàðóøàòñÿ ïðåäïîñûëêè ýòèõ ñîîòíîøåíèé.(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0Dupl:{ m ∈ M }(* M ýòî ëèáî Mp , ëèáî Mq *)begin insert m in M endP0 ≡∧∧∧∧∧∧∧cs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Ñîîòíîøåíèÿ (1-3) è (6) ñîõðàíÿþòñÿ, ò.ê. ýòî äåéñòâèå íåâëèÿåò íà ïåðåìåííûå ýòèõ ñîîòíîøåíèé. Ñîîòíîøåíèÿ (4-5) è(7-8) ñîõðàíÿþòñÿ, ò.ê.
äóáëèðóþùàÿ âñòàâêà ïàêåòà mâîçìîæíà òîëüêî òîãäà, êîãäà ïàêåò m óæå ñîäåðæèòñÿ âêàíàëå; îòñþäà ñëåäóåò, ÷òî ñëåäñòâèÿ ñîîòâåòñòâóþùèõñîîòíîøåíèé óæå áûëè âûïîëíåíû óæå ïåðåä ñàìîé âñòàâêîé.(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0:i do Ut[i] := Ut[i] − δ ; St := St − δ ; Rt := Rt − δif Rt ≤ 0 then delete (Rt, Exp); (* cr := false *)forall h.., ρi ∈ Mp , Mq dobegin ρ := ρ − δ ; if ρ ≤ 0 then remove packet endTime begin forallendP0 ≡∧∧∧∧∧∧∧cs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Ñîîòíîøåíèÿ (1), (2) è (3) ñîõðàíÿþåòñÿ, ò.ê.
çíà÷åíèÿïåðåìåííûõ St , Rt è Ut[i] ìîãóò ëèøü óìåíüøèòüñÿ, è ñåàíññâÿçè ïîëó÷àòåëÿ çàêðûâàåòñÿ, êîãäà çíà÷åíèå Rt ñòàíîâèòñÿðàâíûì 0 .(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0:i do Ut[i] := Ut[i] − δ ; St := St − δ ; Rt := Rt − δif Rt ≤ 0 then delete (Rt, Exp); (* cr := false *)forall h.., ρi ∈ Mp , Mq dobegin ρ := ρ − δ ; if ρ ≤ 0 then remove packet endTime begin forallendP0 ≡∧∧∧∧∧∧∧cs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Ñîîòíîøåíèå (4) ñîõðàíÿåòñÿ, ò.ê.
çíà÷åíèå ρ ìîæåò ëèøüóìåíüøèòüñÿ, è ïàêåò èçûìàåòñÿ, êîãäà çíà÷åíèå åãî ïîëÿ ρñòàíîâèòñÿ ðàâíûì 0 .(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0:i do Ut[i] := Ut[i] − δ ; St := St − δ ; Rt := Rt − δif Rt ≤ 0 then delete (Rt, Exp); (* cr := false *)forall h.., ρi ∈ Mp , Mq dobegin ρ := ρ − δ ; if ρ ≤ 0 then remove packet endTime begin forallendP0 ≡∧∧∧∧∧∧∧cs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High)Äåéñòâèå Time óìåíüøàåò çíà÷åíèÿ âñåõ òàéìåðîâ (è òåõ,êîòîðûå ñîäåðæàòñÿ â ïîëå ρ ïàêåòîâ) íà îäíó è òó æåâåëè÷èíó.
Ïîýòîìó ñîõðàíÿþòñÿ âñå ñîîòíîøåíèÿ âèäàXt ≥ Yt + C , ãäå Xt è Yt òàéìåðû, à C êîíñòàíòà.(1)(2)(3)(4)(5)(6)(7)(8)Èíâàðèàíòíîñòü óòâåðæäåíèÿ P0:i do Ut[i] := Ut[i] − δ ; St := St − δ ; Rt := Rt − δRt ≤ 0 then delete (Rt, Exp); (* cr := false *)forall h.., ρi ∈ Mp , Mq dobegin ρ := ρ − δ ; if ρ ≤ 0 then remove packet endTime begin forallifendP0 ≡∧∧∧∧∧∧∧cs ⇒ St ≤ Scr ⇒ 0 < Rt ≤ R∀i < B + High : Ut[i] ≤ U∀h.., ρi ∈ Mp , Mq : 0 < ρ ≤ µhdata, s, i, w , ρi ∈ Mq ⇒ cs ∧ St ≥ ρ + µ + Rcr ⇒ cs ∧ St ≥ Rt + µhack, i, ρi ∈ Mp ⇒ cs ∧ St > ρhdata, s, i, w , ρi ∈ Mq ⇒ (w = inp [B + i] ∧ i < High) ñîîòíîøåíèè (8) íåò òàéìåðîâ, è ïîýòîìó îíî ñîõðàíÿåòñÿ.(1)(2)(3)(4)(5)(6)(7)(8)Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÏåðâîå òðåáîâàíèå, êîòîðîå ïðåäúÿâëÿåòñÿ êðàññìàòðèâàåìîìó ïðîòîêîëó, ñîñòîèò â òîì, ÷òî êàæäîå ñëîâîäîëæíî áûòü ðàíî èëè ïîçäíî äîñòàâëåíî ïî íàçíà÷åíèþ èëèçàíåñåíî â îò÷åò êàê óòðà÷åííîå.
Îïðåäåëèì ïðåäèêàò Ok(i)ñëåäóþùåé ôîðìóëîéOk(i) ⇔ error [i] = true ∨ ïðîöåññ q âðó÷èë ñëîâî inp [i].Ïîêàæåì, ÷òî ïðîòîêîë íå òåðÿåò íè îäíîãî ñëîâà, íå îòìåòèâýòîãî ôàêòà.Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÒåîðåìà 4.2.Ñëåäóþùåå óòâåðæäåíèå ÿâëÿåòñÿ èíâàðèàíòîì ïðîòîêîëà ñòàéìåðàìè.P1 ≡∧∧∧∧∧∧P0¬ cs =⇒ ∀i < B : Ok(i)(9)cs =⇒ ∀i < B + Low : Ok(i)(10)hdata, true, I , w , ρi ∈ Mq =⇒ ∀i < B + I : Ok(i) (11)cr =⇒ ∀i < B + Exp : Ok(i)(12)hack, I , ρi ∈ Mp =⇒ ∀i < B + I : Ok(i)(13)i1 ≤ i2 < B + High =⇒ Ut[i1 ] ≤ Ut[i2 ](14)Äîêàçàòåëüñòâî.ÑÀÌÎÑÒÎßÒÅËÜÍÎ.Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÑäåëàâ äîïîëíèòåëüíîå äîïóùåíèå, ìû ìîæåì äîêàçàòü òåïåðüïåðâóþ ÷àñòü ñïåöèôèêàöèè ïðîòîêîëà. Áåç ýòîãî äîïóùåíèÿîòïðàâèòåëü ìîæåò îêàçàòüñÿ ÷åðåñ÷óð ¾ëåíèâûì¿ ïðèñîñòàâëåíèè îò÷åòà î ïîòåðÿííûõ ñëîâàõ, à â àëãîðèòìå âñåãîëèøü óêàçàíî, ÷òî ñîîáùåíèå î ïîòåðå íå ìîæåò áûòüñôîðìèðîâàíî â òå÷åíèå 2µ + R åäèíèö âðåìåíè, ñëåäóþùèõçà îêîí÷àíèåì èíòåðâàëà îòïðàâëåíèÿ ñëîâà, íî òàì íå ñêàçàíîî òîì, ÷òî ýòî ñîîáùåíèå ðàíî èëè ïîçäíî îáÿçàíî áûòüñôîðìèðîâàíî.Ïîýòîìó ñäåëàåì äîïîëíèòåëüíîå äîïóùåíèå î òîì, ÷òîäåéñòâèå Ep ðàíî èëè ïîçäíî áóäåò âûïîëíåíî ïðîöåññîì p âðàçóìíûå ñðîêè, ñêàæåì, äî òîãî , êàê Ut[B + Low ] ñòàíåòðàâíûì −2µ − R − λ .Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÒåîðåìà 4.3.
(îá îòñóòñòâèè ïîòåðü)Êàæäîå ñëîâî, ïîÿâèâøååñÿ â ìàññèâå inp , ëèáî âðó÷àåòñÿïðîöåññîì q ïîòðåáèòåëþ, ëèáî ñïóñòÿ íå áîëåå U + 2µ + R + λåäèíèö âðåìåíè ïîñëå ñâîåãî ïîñòóïëåíèÿ îòìå÷àåòñÿïðîöåññîì p êàê óòðà÷åííîå.Çàìå÷àíèÿ1. Ïîä òåðìèíîì ¾ïîñòóïëåíèå ñëîâà¿ ìû ïîäðàçóìåâàåìñðàáàòûâàíèå äåéñòâèÿ Ap ïðîöåññà p , êîòîðîå ðåãèñòðèðóåòî÷åðåäíîå ñëîâî ìàññèâà inp .Äàííàÿ òåîðåìà óòâåðæäàåò, ÷òî íè îäíî ñëîâî, ïîñòóïèâøåå îòãåíåðàòîðà, íå îêàæåòñÿ ¾áåç âåñòè ïðîïàâøèì¿.2.
Óòâåðæäåíèå òåîðåìû äîïóñêàåò âîçìîæíîñòü ñîâìåñòíîãîîñóùåñòâëåíèÿ îáîèõ ñîáûòèé, óïîìÿíóòûõ â ôîðìóëèðîâêå, ñëîâî ìîæåò áûòü óñïåøíî âðó÷åíî ïîòðåáèòåëþ è ïðè ýòîìîòìå÷åíî êàê óòðà÷åíîå.Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÄîêàçàòåëüñòâîÏðè ïîñòóïëåíèè ñëîâà inp [I ] ñðàáàòûâàåò äåéñòâèå Ap .Ïîñëå åãî âûïîëíåíèÿ îêàçûâàåòñÿ âåðíûì íåðàâåíñòâîB + High > I , è îíî áóäåò îñòàâàòüñÿ âåðíûì è äàëåå,ïîñêîëüêó âåëè÷èíà B + High íå óáûâàåò ïðè ðàáîòå ïðîòîêîëà.Åñëè òîò ñåàíñ ñâÿçè, â êîòîðîì ïîñòóïèëî ñëîâî inp [I ] ,çàêðûâàåòñÿ ñïóñòÿ íå áîëåå U + 2µ + R + λ åäèíèö âðåìåíèïîñëå ïîñòóïëåíèÿ ýòîãî ñëîâà, òî ïîñëå âûïîëíåíèÿ äåéñòâèÿçàêðûòèÿ ýòîãî ñåàíñà Cp áóäåò ñïðàâåäëèâî ðàâåíñòâî B > I .Òîãäà óòâåðæäåíèå òåîðåìû ñëåäóåò èç ñîîòíîøåíèÿ (9):¬ cs =⇒ ∀i < B : Ok(i) .Ðàññìîòðèì ñëó÷àé, êîãäà òîò æå ñàìûé ñåàíñ ñâÿçè îñòàåòñÿîòêðûòûì ñïóñòÿ U + 2µ + R + λ åäèíèö âðåìåíè ïîñëåïîñòóïëåíèÿ ñëîâà inp [I ] , è ïîêàæåì, ÷òî â ýòîì ñëó÷àå âåðíîíåðàâåíñòâî B + Low > I .Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÄîêàçàòåëüñòâî (ïðîäîëæåíèå)Äîïóñòèì ïðîòèâíîå: ñïóñòÿ U + 2µ + R + λ åäèíèö âðåìåíèïîñëå ïîñòóïëåíèÿ ñëîâà inp [I ] ñåàíñ îòêðûò è B + Low ≤ I .Òîãäà èç (15): i1 ≤ i2 < B + High =⇒ Ut[i1 ] ≤ Ut[i2 ] ñëåäóåò,÷òî Ut(j) ≤ −R − 2µ − λ âåðíî äëÿ âñåõ j : B + Low ≤ j ≤ I . ñîîòâåòñòâèè ñ ñîãëàøåíèåì î ñâîåâðåìåííîì ñðàáàòûâàíèèäëÿ âñåõ óêàçàííûõ çíà÷åíèé j äîëæíî áûëî ñðàáîòàòüäåéñòâèå Ep .Ïîñêîëüêó ïîñëå âûïîëíåíèÿ äåéñòâèÿ Ep óâåëè÷èâàåòñÿçíà÷åíèÿ Low , ïî çàâåðøåíèè ýòîé ïîñëåäîâàòåëüíîñòèI − (B + Low ) + 1 îáÿçàòåëüíûõ ñðàáàòûâàíèé äåéñòâèÿ Epâåëè÷èíà B + Low äîëæíà ïðåâîñõîäèòü I âîïðåêè äîïóùåíèþ.Çíà÷èò, B + Low > I .
Òîãäà óòâåðæäåíèå òåîðåìû ñëåäóåò èçñîîòíîøåíèÿ (10): cs =⇒ ∀i < B + Low : Ok(i) .Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìè×òîáû óñòàíîâèòü âòîðîå òðåáîâàíèå êîððåêòíîñòè ïðîòîêîëà,íåîáõîäèìî ïîêàçàòü, ÷òî êàæäîå ñëîâî, êîòîðîå áûëî âðó÷åíîïîòðåáèòåëþ, èìååò ïîðÿäêîâûé íîìåð (â ìàññèâå inp )áîëüøèé, ÷åì ðàíåå âðó÷åííîå ñëîâî.Âîñïîëüçóåìñÿ çàïèñüþ pr äëÿ îáîçíà÷åíèÿ ïîðÿäêîâîãîíîìåðà ñàìîãî ïîñëåäíåãî èç âðó÷åííûõ ïîòðåáèòåëþ ñëîâ(äëÿ óäîáñòâà áóäåì ïîëàãàòü, ÷òî âíà÷àëå pr = −1 èUt[−1] = −∞ ).Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÒåîðåìà 4.4.Ñëåäóþùåå óòâåðæäåíèå ÿâëÿåòñÿ èíâàðèàíòîì ïðîòîêîëà ñòàéìåðàìè.P2 ≡∧∧∧∧P1hdata, s, i, w , ρi ∈ Mq =⇒ Ut[B + i] > ρ − µcr =⇒ Rt ≥ Ut[pr ] + µpr < B + High ∧ (Ut[pr ] > −µ =⇒ cr )cr =⇒ B + Exp = pr + 1Äîêàçàòåëüñòâî.ÑÀÌÎÑÒÎßÒÅËÜÍÎ.(15)(16)(17)(18)Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÂñïîìîãàòåëüíàÿ ëåììàÏðè ðàáîòå ïðîòîêîëà âñåãäà ñïðàâåäëèâî ñîîòíîøåíèåhdata, s, i1 , w , ρi ∈ Mq =⇒ (cr ∨ B + i1 > pr )Äîêàçàòåëüñòâî ëåììûÄåéñòâèòåëüíî, ñîãëàñíî ñîîòíîøåíèþ(15): hdata, s, i, w , ρi ∈ Mq =⇒ Ut[B + i] > ρ − µèç hdata, s, i1 , w , ρi ∈ Mq ñëåäóåò Ut[B + i1 ] > ρ − µ > −µ.Åñëè B + i1 ≤ pr , òî, ó÷èòûâàÿ, ÷òî ñîãëàñíî ñîîòíîøåíèþ(14): i1 ≤ i2 < B + High =⇒ Ut[i1 ] ≤ Ut[i2 ]ñïðàâåäëèâî íåðàâåíñòâî pr < B + High ,ïîëó÷àåì íåðàâåíñòâî Ut[pr ] > −µ , èç êîòîðîãî íà îñíîâàíèèñîîòíîøåíèÿ(17): pr < B + High ∧ (Ut[pr ] > −µ =⇒ cr )ñëåäóåò èñòèííîñòü ïðåäèêàòà cr .Êîððåêòíîñòü ïðîòîêîëà ñ òàéìåðàìèÒåîðåìà 4.4.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
