ArchiveEntry "Recitation 2". ProgramVariables. R x. End. Problem. x = -1 -> [ ?x > 0; ] (1 = 0) End. Tactic "Recitation 2: Proof 1". master End. End.