[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