Logica di hoare, dimostrando la regola congiunta dalle regole di base, possibile o no?

Question

(Questo è hw.) Supponiamo di avere queste seguenti regole di prova fornite.

Attualmente sto considerando se posso provare la regola della congiunzione (indicata di seguito) dalle regole logiche Hoare sopra indicate.

La mia risposta sarebbe "no", perché dalle regole di prova della logica Hoare, non posso usare né il Implied regola per dimostrarlo (perché da $ A $ Non posso dedurre $ A wedge b $) né introdurlo ovunque dalle prime quattro regole di prova (l'unica che introduce la congiunzione nella post-condizione richiede un while). Sono abbastanza fiducioso che questa linea di ragionamento sia corretta, ma mi manca qualcosa? Ad esempio, posso discutere sul livello logico proposizionale che da quando ho $ P $ come presupposto, e io l'ho fatto $ Q_1 $ e $ Q_2 $ Come postcondizioni, posso semplicemente introdurre congiunzioni sul livello logico proposizionale (invece di inferire esclusivamente sulla logica di Hoare)?