[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: records

```I've just seen that I can prove the goal as follows:

PHI7.1 :

[-1]    (# b := TRUE,
p := (# n := top!1, h := (# f := FUn!1, s := Sn!1 #) #),
v := 0 #)
= rec!1 WITH [p := prod!1 WITH [n := i!1]]
|-------
[1]    i!1 = top!1

Rule? (case "n(p((# b := TRUE,
p := (# n := top!1, h := (# f := FUn!1, s := Sn!1 #) #),
v := 0 #))) = n(p(rec!1 WITH [p := prod!1 WITH [n := i!1]]))")
Case splitting on
n(p((# b := TRUE,
p := (# n := top!1, h := (# f := FUn!1, s := Sn!1 #) #),
v := 0 #))) = n(p(rec!1 WITH [p := prod!1 WITH [n := i!1]])),
this yields  2 subgoals:
PHI7.1.1 :

{-1}    n(p((# b := TRUE,
p :=
(# n := top!1,
h := (# f := FUn!1, s := Sn!1 #) #),
v := 0 #)))
= n(p(rec!1 WITH [p := prod!1 WITH [n := i!1]]))
[-2]    (# b := TRUE,
p := (# n := top!1, h := (# f := FUn!1, s := Sn!1 #) #),
v := 0 #)
= rec!1 WITH [p := prod!1 WITH [n := i!1]]
|-------
[1]    i!1 = top!1

Rule? (assert)
Simplifying, rewriting, and recording with decision procedures,

This completes the proof of PHI7.1.1.

PHI7.1.2 :

[-1]    (# b := TRUE,
p := (# n := top!1, h := (# f := FUn!1, s := Sn!1 #) #),
v := 0 #)
= rec!1 WITH [p := prod!1 WITH [n := i!1]]
|-------
{1}    n(p((# b := TRUE,
p :=
(# n := top!1,
h := (# f := FUn!1, s := Sn!1 #) #),
v := 0 #)))
= n(p(rec!1 WITH [p := prod!1 WITH [n := i!1]]))
[2]    i!1 = top!1

Rule? (replace -1)
Replacing using formula -1,
this simplifies to:
PHI7.1.2 :

[-1]    (# b := TRUE,
p := (# n := top!1, h := (# f := FUn!1, s := Sn!1 #) #),
v := 0 #)
= rec!1 WITH [p := prod!1 WITH [n := i!1]]
|-------
{1}    n(p(rec!1 WITH [p := prod!1 WITH [n := i!1]]))
= n(p(rec!1 WITH [p := prod!1 WITH [n := i!1]]))
[2]    i!1 = top!1

which is trivially true.

This completes the proof of PHI7.1.2.

But I am still puzzled of this complicated proof for such a trivial
goal. Is there any other simpler proof ?

Monica

```