KeY Logic Documentation

Defined symbols in the KeY System

Generated from version: heads/main on Fri Aug 21 01:50:47 UTC 2026

Overview

wdReachRules.key

Taclets

Enabled under choices: wdChecks:on

wd_Reach_Pred_Acc

wd_Reach_Pred_Acc { \find ( WD ( acc ( h , l , o , p ) ) ) \replacewith ( wd ( h ) & wd ( l ) & wd ( o ) & wd ( p ) & wellFormed ( h ) ) \heuristics (simplify ) };defined in: wdReachRules.key Line: 13 Offset :4

wd_Reach_Pred_Reach

wd_Reach_Pred_Reach { \find ( WD ( reach ( h , l , o , p , i ) ) ) \replacewith ( wd ( h ) & wd ( l ) & wd ( o ) & wd ( p ) & wd ( i ) & wellFormed ( h ) ) \heuristics (simplify ) };defined in: wdReachRules.key Line: 24 Offset :4