% Theorem in kd45 (half 2) % box(or(P,diam(Q))) <= or(box(P),diam(Q)). '$box'('$or'(p,'$diam'(q)))-w -> []. '$or'('$box'(p),'$diam'(q))-w. :-option(term_var_weight). /* Proof: ====== 3 : r(C,D) -> r(E,D) [axiom] 4 : C-D -> $or(C,E)-D [axiom] 5 : C-D -> $or(E,C)-D [axiom] 6 : $or(C,D)-E -> C-E,D-E [axiom] 7 : C-D,$not(C)-D [axiom] 8 : C-D,$not(C)-D -> [axiom] 9 : $diam(C)-D -> C-g(C,D) [axiom] 10 : $diam(C)-D -> r(D,g(C,D)) [axiom] 11 : r(C,D),E-D -> $diam(E)-C [axiom] 12 : $box(C)=$not($diam($not(C))) [axiom] 14 : $box($or(p,$diam(q)))-w -> [axiom] 15 : $or($box(p),$diam(q))-w [axiom] 16 : $not($diam($not($or(p,$diam(q)))))-w -> [reduction of 14 by [12]] 17 : $or($not($diam($not(p))),$diam(q))-w [reduction of 15 by [12]] 22 : $diam($not($or(p,$diam(q))))-w [negative chaining of 7 from 16] 23 : $not($or(p,$diam(q)))-g($not($or(p,$diam(q))),w) [negative chaining of 22 from 9] 24 : r(w,g($not($or(p,$diam(q))),w)) [negative chaining of 22 from 10] 25 : r(C,g($not($or(p,$diam(q))),w)) [negative chaining of 24 from 3] 42 : r(C,D),E-D -> E-g(E,C) [negative chaining of 11 from 9] 43 : r(C,D),E-D -> r(C,g(E,C)) [negative chaining of 11 from 10] 51 : r(C,D),E-D -> $or(F,$diam(E))-C [negative chaining of 11 from 5] 56 : r(C,g($not($or(p,$diam(q))),w)) -> $not($or(p,$diam(q)))-g($not($or(p,$diam(q))),C) [negative chaining of 23 from 42] 57 : $not($or(p,$diam(q)))-g($not($or(p,$diam(q))),C) [reduction of 56 by [25]] 58 : $or(p,$diam(q))-g($not($or(p,$diam(q))),C) -> [negative chaining of 57 from 8] 74 : r(C,g($not($or(p,$diam(q))),D)) -> r(C,g($not($or(p,$diam(q))),C)) [negative chaining of 57 from 43] 98 : $not($diam($not(p)))-w,$diam(q)-w [negative chaining of 17 from 6] 99 : $diam($not(p))-w -> $diam(q)-w [negative chaining of 98 from 8] 100 : r(w,C),$not(p)-C -> $diam(q)-w [negative chaining of 11 from 99] 101 : r(w,C),$not(p)-C -> q-g(q,w) [negative chaining of 100 from 9] 102 : r(w,C),$not(p)-C -> r(w,g(q,w)) [negative chaining of 100 from 10] 107 : r(w,C) -> p-C,q-g(q,w) [negative chaining of 7 from 101] 108 : r(w,C) -> p-C,r(w,g(q,w)) [negative chaining of 7 from 102] 109 : r(w,C) -> q-g(q,w),$or(p,D)-C [negative chaining of 107 from 4] 115 : r(w,C) -> r(w,g(q,w)),$or(p,D)-C [negative chaining of 108 from 4] 157 : r(w,g($not($or(p,$diam(q))),C)) -> q-g(q,w) [negative chaining of 109 from 58] 160 : r(w,g($not($or(p,$diam(q))),C)),r(D,g(q,w)) -> q-g(q,D) [negative chaining of 157 from 42] 170 : r(w,g($not($or(p,$diam(q))),C)) -> r(w,g(q,w)) [negative chaining of 115 from 58] 172 : r(w,g(q,w)) [negative chaining of 25 from 170] 173 : r(C,g(q,w)) [negative chaining of 172 from 3] 175 : r(w,g($not($or(p,$diam(q))),C)) -> q-g(q,D) [reduction of 160 by [173]] 296 : r(g($not($or(p,$diam(q))),C),D),q-D -> [negative chaining of 51 from 58] 364 : r(w,g($not($or(p,$diam(q))),C)),r(g($not($or(p,$diam(q))),D),g(q,E)) -> [negative chaining of 175 from 296] 365 : r(C,g($not($or(p,$diam(q))),C)) [negative chaining of 25 from 74] 366 : r(C,g($not($or(p,$diam(q))),D)) [negative chaining of 365 from 3] 367 : q-g(q,C) [reduction of 175 by [366]] 376 : r(g($not($or(p,$diam(q))),C),g(q,D)) -> [reduction of 364 by [366]] 384 : r(C,g(q,D)) -> r(C,g(q,C)) [negative chaining of 367 from 43] 385 : r(C,g(q,C)) [negative chaining of 173 from 384] 386 : r(C,g(q,D)) [negative chaining of 385 from 3] 387 : false [reduction of 376 by [386]] Length = 50, Depth = 17 Total time: 152820 milliseconds */