race_winner
Two boys decided to compete in text typing on the site "Key races". During the competition, they have to type a text consisting of s characters. The first participant types one character in v1 milliseconds and has ping t1 milliseconds. The second participant types one character in v2 milliseconds and has ping t2 milliseconds. If connection ping (delay) is t milliseconds, the competition passes for a participant as follows: 1. Exactly after t milliseconds after the start of the competition the participant receives the text to be entered. 2. Right after that he starts to type it. 3. Exactly t milliseconds after he ends typing all the text, the site receives information about it. The winner is the participant whose information on the success comes earlier. If the information comes from both participants at the same time, it is considered that there is a draw. Given the length of the text and the information about participants, determine the result of the game. Input The first line contains five integers s, v1, v2, t1, t2 (1 ≤ s, v1, v2, t1, t2 ≤ 1000) — the number of characters in the text, the time of typing one character for the first participant, the time of typing one character for the the second participant, the ping of the first participant and the ping of the second participant. Output If the first participant wins, print "First". If the second participant wins, print "Second". In case of a draw print "Friendship". Examples Input 5 1 2 1 2 Output First Input 3 3 1 1 1 Output Second Input 4 5 3 1 5 Output Friendship Note In the first example, information on the success of the first participant comes in 7 milliseconds, of the second participant — in 14 milliseconds. So, the first wins. In the second example, information on the success of the first participant comes in 11 milliseconds, of the second participant — in 5 milliseconds. So, the second wins. In the third example, information on the success of the first participant comes in 22 milliseconds, of the second participant — in 22 milliseconds. So, it is be a draw.
Function Signature
def race_winner (s v1 v2 t1 t2 : Nat) : String
Theorem Signature
def get_total_time (s v t : Nat) : Nat :=
t + s * v + t
def winner_to_string (time1 time2 : Nat) : String :=
if time1 < time2 then "First"
else if time2 < time1 then "Second"
else "Friendship"
def race_winner_prop (s v1 v2 t1 t2 : Nat) (out : String) : Prop :=
let time1 := get_total_time s v1 t1
let time2 := get_total_time s v2 t2
out = winner_to_string time1 time2
theorem race_winner_spec (s v1 v2 t1 t2 : Nat) : race_winner_prop s v1 v2 t1 t2 (race_winner s v1 v2 t1 t2)
Please log in or register to submit a solution for this challenge.