ArchiveEntry "GPWS Bad Model". ProgramVariables. R x. R y. End. Problem. x=0 & y = 1 -> [{x'= 1, y'= 2*x}] (y = x^4 + 1) End. Tactic "GPWS Bad Model: Proof 1". master partial End. End. ArchiveEntry "GPWS Good Model". ProgramVariables. R x. R y. End. Problem. x = 0 & y = 1 -> [{x' = 1, y' = 2*x}]y = x^2 + 1 End. Tactic "GPWS Good Model: Proof 1". dI(1.1) ; master End. End.