semantics: proof of the construction of the inverse image using an inductive predicate

I have to code the following problem in a test wizard and I am really stuck in the strategy to use. Essentially, this is called reverse image construction for a well-founded relationship, although my problem is the particular case.

Given two sets of states in different systems $ A $ Y $ B $, consider binary relationships $ r subseteq A times A, r & # 39; subseteq B times B, R subseteq A times B $. We say that a state $ s $ It is ending with respect to the relationship. $ r $ and we write $ t ; s ; r $ Yes $ forall s & # 39; .r ^ {++} s ; s & # 39; implies t ; s & # 39; ; r $. Of course, this models the notion of termination relationship. The base case is given by states without exit transitions, and for them, we add states that only make the transition to final states.

We present a property that basically will say that system. $ A $ is simulated by system $ B $. $ for all a ; b ; a & # 39; R ; a ; b ; land r ; a ; a & # 39; implies exists b & # 39; . R ; a & # 39; ; b & # 39; land r & # 39; ; b ; b & # 39; $. You may want to draw a square diagram of this formula.

The problem is to show that if $ t ; b ; r & # 39; $ then we have that $ t ; a ; r $ Given the $ R ; a ; b $ and the simulation property above. This is quite intuitive. If you had an infinite chain in $ A $ this would be induced to an infinite chain in $ B $ but $ b $ is ending and we get a contradiction. However, it is not so clear how to implement this in a test assistant since we have formulated the notion of termination with a inductive predicate. I think there could be two approaches to this:

  1. Demonstrate formally the previous reasoning that should lead to some objective of the form. This would work by contradiction. $ lnot t ; a & # 39; ; r = exists to & # 39; & # 39 ;. r ^ {++} a & # 39; ; a & # 39; & # 39; land lnot t ; a & # 39; & # 39; ; r $ This should be used to prove some goal like $ forall i in mathbb {N}. exists a_i, b_i. R ; a_i ; b_i land b_ {i-1} a + b_i, a_ {i-1} a + a_i $. My intention tells me that this will be quite difficult since I am imposing myself to work with infinite sequences.

  2. The second approach would be to use an equivalent characterization of foundation as the characterization of the minimum element and try to deduce from the goal.

Could you tell me which approach you think is feasible and the key steps I will need to show in the testing assistant?