KeY Logic Documentation

Defined symbols in the KeY System

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

Overview

genericRules.key

Sorts

G

\generic G, S1, S2, H;defined in: genericRules.key Line: 10 Offset :4

S1

\generic G, S1, S2, H;defined in: genericRules.key Line: 10 Offset :4

S2

\generic G, S1, S2, H;defined in: genericRules.key Line: 10 Offset :4

H

\generic G, S1, S2, H;defined in: genericRules.key Line: 10 Offset :4

GSub

\generic GSub \extends G ;defined in: genericRules.key Line: 11 Offset :4

C

\generic C;defined in: genericRules.key Line: 13 Offset :4

CSub

\generic CSub \extends C ;defined in: genericRules.key Line: 14 Offset :4

Taclets

No choice condition specified

firstOfPair

firstOfPair { \find ( first ( pair ( t , t1 ) ) ) \replacewith ( t ) \heuristics (concrete ) };defined in: genericRules.key Line: 47 Offset :4

secondOfPair

secondOfPair { \find ( second ( pair ( t , t1 ) ) ) \replacewith ( t1 ) \heuristics (concrete ) };defined in: genericRules.key Line: 53 Offset :4

instanceof_static_type

instanceof_static_type { \schemaVar \term any a ; \find ( instance <[ G ]> ( a ) ) \varcond \replacewith ( TRUE ) \heuristics (concrete , evaluate_instanceof ) \displayname "instanceof static supertype" };defined in: genericRules.key Line: 61 Offset :4

instanceof_static_type_2

instanceof_static_type_2 { \schemaVar \term any a , a2 ; \assumes ( a2 = a ==> ) \find ( instance <[ G ]> ( a ) ) \varcond \replacewith ( TRUE ) \heuristics (concrete , evaluate_instanceof ) \displayname "instanceof static supertype" };defined in: genericRules.key Line: 70 Offset :4

instanceof_not_compatible

instanceof_not_compatible { \schemaVar \term any a ; \find ( instance <[ G ]> ( a ) = TRUE ) \varcond \replacewith ( a = null ) \heuristics (concrete , evaluate_instanceof ) \displayname "instanceof disjoint type" };defined in: genericRules.key Line: 80 Offset :4

instanceof_not_compatible_2

instanceof_not_compatible_2 { \schemaVar \term any a ; \find ( instance <[ G ]> ( a ) = FALSE ) \varcond \replacewith ( ! ( a = null ) ) \heuristics (concrete , evaluate_instanceof ) \displayname "instanceof disjoint type" };defined in: genericRules.key Line: 89 Offset :4

instanceof_not_compatible_3

instanceof_not_compatible_3 { \schemaVar \term any a ; \find ( instance <[ G ]> ( a ) = TRUE ) \varcond \replacewith ( false) \heuristics (concrete , evaluate_instanceof ) \displayname "instanceof disjoint type" };defined in: genericRules.key Line: 98 Offset :4

instanceof_not_compatible_4