theory EX_RecMult_deep  = SALOverflowFWInst_deep:

section {* SAL Example: Multiplication*}

text {* This example is about a program that multplies 
variable C1 with C2 and writes the result to C3. *}

subsection {* Program Variables *}


text {*
The variables
C1, C2, C3 are just abbreviations for the addresses 1, 2 and 3. 
*}

constdefs 
  C1 :: nat -- "cell1"
 "C1 \<equiv> 1"
  C2 :: nat -- "cell2"
 "C2 \<equiv> 2"  
  C3 :: nat -- "cell3"
 "C3 \<equiv> 3"

text {* At some point in the program we need to check whether a variable contains number one or zero. Since conditional
jumps in SAL expect their arguments in form of variables, we introduce variables Zero and One. The progam uses them to the constants NAT 0 and NAT 1. *}

constdefs
  Zero::nat -- "stores NAT 0"
 "Zero \<equiv> 4"
  One:: nat -- "stores NAT 1"
 "One \<equiv> 5"

text {* Our program will do multiplication by recursively 
calling a procedure that decrements C1 and adds C2 to C3. Whenever 
this procedure is called, the return address, which is the current address 
incremented by one, is dumped in a variable r. The address of r, which is 6, is kept in the variable Ra. *}

constdefs
  r :: nat -- "return address buffer"
 "r \<equiv> 6"
  Ra :: nat -- "stores the address of R"
  "Ra \<equiv> 7"

text {* The program maintains a stack of return addresses. This stack starts at address Soff and grows towards higher
addresses. The variable S contains the stack pointer. This is the address, where the next element of the stack
is going to be stored. *}

constdefs 
  S:: nat -- "stack pointer"
  "S \<equiv> 8"
  Soff:: nat --"stack base" 
  "Soff \<equiv> 9"

text {* Since SAL programs are executed on a default initial state, we have to simulate the
input phase of the program by SET operations. In this example we analyse the program for
inputs arg1 and arg2. *}

constdefs 
 arg1::nat
 "arg1\<equiv>2"
 arg2::nat
 "arg2\<equiv>3"

subsection {* Program Code *}

text {* 
Next, we present the program without annotations.
\begin{tabbing}
@{text "prog = [ (0, ["} ~ ~ ~ \= Procedure 0 (Startup) \\
@{text "SET Zero 0,"} \= Initialise Zero with NAT 0. \\
@{text "SET One 1,"}         \> Initialise One with NAT 1. \\  
@{text "SET POS r,"}          \> Initialise POS with NAT r (r = 6). \\
@{text "SET S Soff,"}        \> Initialise S with NAT Soff (Soff = 9). \\
@{text "SET C1 arg1,"}       \> Initialise Argument C1 with NAT arg1. \\
@{text "SET C2 arg2,"}       \> Initialise Argument C2 with NAT arg2. \\
@{text "SET C3 0,"}          \> Initialise Result Variable C3 with NAT 0. \\
@{text "CALL r 1,"}          \> Start multplication procedure.\\
@{text "HALT ]), "}          \> Stop execution \\
\\
@{text "(1,["}               \> Procedure 1 (Multiplication)\\
@{text "MOV Ra S,"}          \> Push the return address onto the Stack. \\
@{text "JMPEQ C1 Zero 7,"}   \> If C1 is NAT 0 we are done, otherwise . . . \\
@{text "SUB C1 One,"}\\      \> . . . we decrement C1 \\
@{text "ADD C3 C2,"}         \> and add C2 to the result variable C3. \\
@{text "INC S,"}             \> We increment the stack pointer, before . \\
@{text "CALL r 1,"}           \> we do the recursive call. \\
@{text "SUB S One,"}          \> After return we restore the old stack pointer \\
@{text "MOV S Ra,"}           \> and copy the return address from the stack to r.\\
@{text "RET r ]) ]"}         \> We finish this call by returning to the caller.
\end{tabbing} 
*}

subsection {* Program with Annotations *}
 
constdefs
  prog :: "SALprogram"
 "prog \<equiv> [
(0, [ (SET Zero 0,None),
      (SET One 1,None),
      (SET Ra r,None),
      (SET S Soff,None),
      (SET C1 arg1,None),
      (SET C2 arg2,None),
      (SET C3 0,None),
      (CALL r 1,Some (\<Lambda> [(V C1 \<doteq> C (NAT arg1)),
                         (V C2 \<doteq> C (NAT arg2)),
                         (V C3 \<doteq> C (NAT 0)),
                         (V Zero \<doteq> C (NAT 0)),
                         (V One \<doteq> C (NAT 1)),
                         (V Ra \<doteq> C (NAT r)),
                         (V S \<doteq> C (NAT Soff)), 
                         (\<Prod> 0. (\<Lambda> [ Neg (Lv 0 \<doteq> (C (NAT C1))),
                                    Neg (Lv 0 \<doteq> (C (NAT C2))),
                                    Neg (Lv 0 \<doteq> (C (NAT C3))),
                                    Neg (Lv 0 \<doteq> (C (NAT Zero))),
                                    Neg (Lv 0 \<doteq> (C (NAT One))),
                                    Neg (Lv 0 \<doteq> (C (NAT Ra))),
                                    Neg (Lv 0 \<doteq> (C (NAT S)))]) \<supset> ((Deref (Lv 0)) \<doteq> (Old (Deref (Lv 0)))))])),
                                
      (JMPB 0, Some  (V C3 \<doteq> (C (NAT arg1)) \<odot> (C (NAT arg2))))]),
(1,[ (MOV Ra S,Some (\<Lambda> [ Ty (V C1) Nat, Ty (V C2) Nat, Ty (V C3) Nat,
                         ((V C3) \<oplus> ((V C1) \<odot> (V C2))) \<preceq> (C (NAT MAX)),
                         (V Zero) \<doteq> (C (NAT 0)),
                         (V One) \<doteq> (C (NAT 1)),
                         (V Ra) \<doteq> (C (NAT r)),
                         Ty (V S) Nat, (C (NAT Soff)) \<preceq> (V S),
                         ((V S) \<oplus> (V C1)) \<preceq> C (NAT MAX),
                         (V r) \<doteq>  Rp,
                         (\<Prod> 0. (Neg (Lv 0 \<doteq> (C (NAT r)))) \<supset> ((Deref (Lv 0)) \<doteq> (Old (Deref (Lv 0)))))])),
                     
     (JMPEQ C1 Zero 7,None),
     (SUB C1 One,None),
     (ADD C3 C2,None),
     (INC S,None),
     (CALL r 1,Some (\<Lambda> [ Ty (V C1) Nat, Ty (V C2) Nat, Ty (V C3) Nat,
                         Ty (Old (V C1)) Nat, Ty (Old (V C2)) Nat,  Ty (Old (V C3)) Nat,
                         (C (NAT 0)) \<prec> (Old (V C1)), 
                         (V C1) \<doteq> Old ((V C1) \<ominus> (C (NAT 1))),
                         (V C2) \<doteq> Old (V C2),
                         (V C3) \<doteq> Old ((V C3) \<oplus> (V C2)), 
                         ((V C3) \<oplus> ((V C1) \<odot> (V C2))) \<preceq> (C (NAT MAX)),
                         (V Zero) \<doteq> (C (NAT 0)),
                         (V One) \<doteq> (C (NAT 1)),
                         (V Ra) \<doteq> (C (NAT r)),
                         Ty (V S) Nat,
                         (C (NAT Soff)) \<preceq> (V S),
                         Ty (Old (V S)) Nat,
                         (V S) \<doteq> Old ((V S) \<oplus> (C (NAT 1))), 
                         Deref (Old (V S)) \<doteq> Rp,
                         ((V S) \<oplus> (V C1)) \<preceq> (C (NAT MAX)),
                         \<Prod> 0. ((\<Lambda> [ Neg ((Lv 0) \<doteq> C (NAT r)),
                                   Neg ((Lv 0) \<doteq> C (NAT S)),
                                   Neg ((Lv 0) \<doteq> C (NAT C1)),
                                   Neg ((Lv 0) \<doteq> C (NAT C3)), 
                                   (((Lv 0)) \<oplus> (C (NAT 1))) \<prec> (V S)]) \<supset> 
                                     ((Deref (Lv 0)) \<doteq> (Old (Deref (Lv 0)))))])),
     (SUB S One,Some (\<Lambda> [ Ty (V C3) Nat, 
                          Ty (Old (V C3)) Nat,
                          Ty (Old (V C1)) Nat,
                          Ty (Old (V C2)) Nat,
                          (V C3) \<doteq> Old ((V C3) \<oplus> ((V C1) \<odot> (V C2))),
                          (V Zero) \<doteq> (C (NAT 0)),
                          (V One) \<doteq> (C (NAT 1)),
                         (V Ra) \<doteq> (C (NAT r)),
                         Ty (V S) Nat,
                         (C (NAT Soff)) \<preceq> (V S),
                         Ty (Old (V S)) Nat,
                         (V S) \<doteq> Old ((V S) \<oplus> (C (NAT 1))), 
                         Deref (Old (V S)) \<doteq> Rp,
                         ((V S) \<oplus> (V C1)) \<preceq> (C (NAT MAX)),
                         \<Prod> 0. ((\<Lambda> [ Neg ((Lv 0) \<doteq> C (NAT r)),
                                   Neg ((Lv 0) \<doteq> C (NAT S)),
                                   Neg ((Lv 0) \<doteq> C (NAT C1)),
                                   Neg ((Lv 0) \<doteq> C (NAT C3)),
                                   (((Lv 0)) \<oplus> (C (NAT 1))) \<prec> (V S)]) \<supset> 
                                      ((Deref (Lv 0)) \<doteq> (Old (Deref (Lv 0)))))])),

                     
     (MOV S Ra,None),
     (RET r,Some (\<Lambda> [ Ty (V C3) Nat, 
                          Ty (Old (V C3)) Nat,
                          Ty (Old (V C1)) Nat,
                          Ty (Old (V C2)) Nat,
                          (V C3) \<doteq> Old ((V C3) \<oplus> ((V C1) \<odot> (V C2))),
                          (V Zero) \<doteq> (C (NAT 0)),
                          (V One) \<doteq> (C (NAT 1)),
                         (V Ra) \<doteq> C (NAT r),
                         (V r) \<doteq> Rp,
                         Ty (V S) Nat,
                         (C (NAT Soff)) \<preceq> (V S),
                         ((V S) \<oplus> (V C1)) \<preceq> (C (NAT MAX)),
                         (V S) \<doteq> Old (V S),
                         \<Prod> 0. ((\<Lambda> [ Neg ((Lv 0) \<doteq> C (NAT r)),
                                     Neg ((Lv 0) \<doteq> C (NAT S)),
                                   Neg ((Lv 0) \<doteq> C (NAT C1)),
                                   Neg ((Lv 0) \<doteq> C (NAT C3)),
                                   (Lv 0) \<prec> (V S)]) \<supset> 
                                      ((Deref (Lv 0)) \<doteq> (Old (Deref (Lv 0)))))]))    
   ])  
]"

subsection {* The Verification Condition *}


generate_code [term_of]
  vcg = "vcgSALDeep"
  prg = "prog" 

ML {* set show_brackets; *}
ML {* val vc = vcg prog; *}
ML {* File.write (Path.unpack "pvc.txt") (Pretty.str_of (Sign.pretty_term (sign_of (the_context ())) (term_of_form vc))); *}
ML {* val pvc = (Pretty.str_of (Sign.pretty_term (sign_of (the_context ())) (term_of_form vc))); *}
ML {* reset show_brackets *}


constdefs
vc::"SALform"
"vc \<equiv> (\<Lambda> [((\<Lambda> [(Pc \<doteq> (C (POS (0, 0)))), (\<Prod>0. ((Deref (Lv 0)) \<doteq> (C ILLEGAL))), (\<Prod>0. ((Old (Deref (Lv 0))) \<doteq> (C ILLEGAL))), (Rp \<doteq> (C (POS (0, 0)))), (Tm \<doteq> (C (NAT 0)))]) \<supset> (\<Lambda> [((C (NAT 0)) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), ((Pc \<doteq> (C (POS (0, 0)))) \<supset> (\<Lambda> [((C (NAT (Suc 0))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), (((C (POS (0, (Suc 0)))) \<doteq> (C (POS (0, (Suc 0))))) \<supset> (\<Lambda> [((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), (((C (POS (0, (Suc (Suc 0))))) \<doteq> (C (POS (0, (Suc (Suc 0)))))) \<supset> (\<Lambda> [((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), (((C (POS (0, (Suc (Suc (Suc 0)))))) \<doteq> (C (POS (0, (Suc (Suc (Suc 0))))))) \<supset> (\<Lambda> [((C (NAT (Suc (Suc 0)))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), 
(((C (POS (0, (Suc (Suc (Suc (Suc 0))))))) \<doteq> (C (POS (0, (Suc (Suc (Suc (Suc 0)))))))) \<supset> (\<Lambda> [((C (NAT (Suc (Suc (Suc 0))))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), (((C (POS (0, (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (C (POS (0, (Suc (Suc (Suc (Suc (Suc 0))))))))) \<supset> (\<Lambda> [((C (NAT 0)) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), (((C (POS (0, (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (POS (0, (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) \<supset> (\<Lambda> [T, (\<Lambda> [((C (NAT (Suc (Suc 0)))) \<doteq> (C (NAT (Suc (Suc 0))))), ((C (NAT (Suc (Suc (Suc 0))))) \<doteq> (C (NAT (Suc (Suc (Suc 0)))))), ((C (NAT 0)) \<doteq> (C (NAT 0))), ((C (NAT 0)) \<doteq> (C (NAT 0))), ((C (NAT (Suc 0))) \<doteq> (C (NAT (Suc 0)))), ((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))), ((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))), (\<Prod>0. ((\<Lambda> [(Neg ((Lv 0) \<doteq> (C (NAT (Suc 0))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc 0)))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc 0))))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc 0)))))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc 0))))))))), 
(Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))]) \<supset> ((IF (Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc 0))))) THEN (C (NAT 0)) ELSE (IF (Lv 0) \<doteq> (C (NAT (Suc (Suc 0)))) THEN (C (NAT (Suc (Suc (Suc 0))))) ELSE (IF (Lv 0) \<doteq> (C (NAT (Suc 0))) THEN (C (NAT (Suc (Suc 0)))) ELSE (IF (Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))) ELSE (IF (Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) THEN (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) ELSE (IF (Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc 0))))))) THEN (C (NAT (Suc 0))) ELSE (IF (Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc 0)))))) THEN (C (NAT 0)) ELSE (Deref (Lv 0))))))))) \<doteq> (Old (Deref (Lv 0))))))])]))]))]))]))]))]))]))])), (\<Lambda> [((\<Lambda> [(\<Lambda> [T, (\<Lambda> [((V (Suc 0)) \<doteq> (C (NAT (Suc (Suc 0))))), ((V (Suc (Suc 0))) \<doteq> (C (NAT (Suc (Suc (Suc 0)))))), ((V (Suc (Suc (Suc 0)))) \<doteq> (C (NAT 0))), ((V (Suc (Suc (Suc (Suc 0))))) \<doteq> (C (NAT 0))), ((V (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc 0)))), 
((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))), ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))), (\<Prod>0. ((\<Lambda> [(Neg ((Lv 0) \<doteq> (C (NAT (Suc 0))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc 0)))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc 0))))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc 0)))))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc 0))))))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))]) \<supset> ((Deref (Lv 0)) \<doteq> (Old (Deref (Lv 0))))))])]), (Pc \<doteq> (C (POS (0, (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))]) \<supset> (\<Lambda> [(\<Lambda> [(Ty (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) vtype.Nat), (Ty (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) vtype.Nat)]), (\<Lambda> [(Ty (V (Suc 0)) vtype.Nat), (Ty (V (Suc (Suc 0))) vtype.Nat), (Ty (V (Suc (Suc (Suc 0)))) vtype.Nat), (((V (Suc (Suc (Suc 0)))) \<oplus> ((V (Suc 0)) \<odot> (V (Suc (Suc 0))))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), ((V (Suc (Suc (Suc (Suc 0))))) \<doteq> (C (NAT 0))), ((V (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc 0)))), 
((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))), (Ty (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) vtype.Nat), ((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))) \<preceq> (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))), (((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<oplus> (V (Suc 0))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), ((C (POS (0, (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))) \<doteq> (C (POS (0, (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))), (\<Prod>0. ((Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) \<supset> ((IF (Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) THEN (C (POS (0, (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))) ELSE (Deref (Lv 0))) \<doteq> (Deref (Lv 0)))))])]))]), (\<Lambda> [((\<Lambda> [(\<Lambda> [T, ((V (Suc (Suc (Suc 0)))) \<doteq> ((C (NAT (Suc (Suc 0)))) \<odot> (C (NAT (Suc (Suc (Suc 0)))))))]), (Pc \<doteq> (C (POS (0, (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))]) \<supset> (\<Lambda> [T, ((V (Suc (Suc (Suc 0)))) \<doteq> ((C (NAT (Suc (Suc 0)))) \<odot> (C (NAT (Suc (Suc (Suc 0)))))))]))]), (\<Lambda> [((\<Lambda> [(\<Lambda> [(\<Lambda> [(Ty (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) vtype.Nat), (Ty (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) vtype.Nat)]), 
(\<Lambda> [(Ty (V (Suc 0)) vtype.Nat), (Ty (V (Suc (Suc 0))) vtype.Nat), (Ty (V (Suc (Suc (Suc 0)))) vtype.Nat), (((V (Suc (Suc (Suc 0)))) \<oplus> ((V (Suc 0)) \<odot> (V (Suc (Suc 0))))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), ((V (Suc (Suc (Suc (Suc 0))))) \<doteq> (C (NAT 0))), ((V (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc 0)))), ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))), (Ty (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) vtype.Nat), ((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))) \<preceq> (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))), (((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<oplus> (V (Suc 0))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), ((V (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> Rp), (\<Prod>0. ((Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) \<supset> ((Deref (Lv 0)) \<doteq> (Old (Deref (Lv 0))))))])]), 
(Pc \<doteq> (C (POS ((Suc 0), 0))))]) \<supset> (\<Lambda> [(\<Lambda> [(Ty (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc 0))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc 0))) vtype.Nat), (Ty (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc 0)))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc 0)))))) vtype.Nat)]), ((\<Lambda> [(Ty (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc 0))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc 0))) vtype.Nat), (Ty (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc 0)))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc 0)))))) vtype.Nat), ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc 0))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc 0))) \<doteq> (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc 0)))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc 0))))))), ((C (POS ((Suc 0), (Suc 0)))) \<doteq> (C (POS ((Suc 0), (Suc 0)))))]) \<supset> (\<Lambda> [(\<Lambda> [((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> 
(C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> Rp), (Ty (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) Pos)]), (\<Lambda> [(Ty (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc 0))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc 0))))) vtype.Nat), (Ty (Old (V (Suc (Suc (Suc 0))))) vtype.Nat), (Ty (Old (V (Suc 0))) vtype.Nat), (Ty (Old (V (Suc (Suc 0)))) vtype.Nat), ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc 0))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc 0))))) \<doteq> (Old ((V (Suc (Suc (Suc 0)))) \<oplus> ((V (Suc 0)) \<odot> (V (Suc (Suc 0))))))), ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc 0)))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT 0))), 
((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc 0))))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> (C (NAT (Suc 0)))), ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))), ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> Rp), (Ty (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) vtype.Nat), ((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))) \<preceq> (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))), 
(((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) \<oplus> (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc 0))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc 0)))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) \<doteq> (Old (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))), (\<Prod>0. ((\<Lambda> [(Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc 0))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc 0))))))), ((Lv 0) \<prec> (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))]) \<supset> ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (Lv 0) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (Deref (Lv 0))) \<doteq> (Old (Deref (Lv 0))))))])])), 
((\<Lambda> [(Ty (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc 0))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc 0))) vtype.Nat), (Ty (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc 0)))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc 0)))))) vtype.Nat), (Neg ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc 0))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc 0))) \<doteq> (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc 0)))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc 0)))))))), ((C (POS ((Suc 0), (Suc 0)))) \<doteq> (C (POS ((Suc 0), (Suc 0)))))]) \<supset> (\<Lambda> [(\<Lambda> [(Ty (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc 0))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc 0))) vtype.Nat), (Ty (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc 0))))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc 0))))))) vtype.Nat)]), (((C (POS ((Suc 0), (Suc (Suc 0))))) \<doteq> (C (POS ((Suc 0), 
(Suc (Suc 0)))))) \<supset> (\<Lambda> [(((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc 0))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc 0))))) \<oplus> (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc 0)))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc 0))))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), (((C (POS ((Suc 0), (Suc (Suc (Suc 0)))))) \<doteq> (C (POS ((Suc 0), (Suc (Suc (Suc 0))))))) \<supset> (\<Lambda> [((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) \<prec> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), (((C (POS ((Suc 0), (Suc (Suc (Suc (Suc 0))))))) \<doteq> (C (POS ((Suc 0), (Suc (Suc (Suc (Suc 0)))))))) \<supset> (\<Lambda> [T, (\<Lambda> [(Ty ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc 0))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc 0))) \<ominus> (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc 0))))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc 0)))))))) vtype.Nat), (Ty (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> 
(C (NAT (Suc (Suc 0)))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc 0)))) vtype.Nat), (Ty ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc 0))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc 0))))) \<oplus> (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc 0)))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc 0))))) vtype.Nat), (Ty (Old (V (Suc 0))) vtype.Nat), (Ty (Old (V (Suc (Suc 0)))) vtype.Nat), (Ty (Old (V (Suc (Suc (Suc 0))))) vtype.Nat), ((C (NAT 0)) \<prec> (Old (V (Suc 0)))), (((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc 0))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc 0))) \<ominus> (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc 0))))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (Old ((V (Suc 0)) \<ominus> (C (NAT (Suc 0)))))), ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc 0)))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc 0)))) \<doteq> (Old (V (Suc (Suc 0))))), (((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> 
(C (NAT (Suc (Suc (Suc 0))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc 0))))) \<oplus> (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc 0)))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc 0))))) \<doteq> (Old ((V (Suc (Suc (Suc 0)))) \<oplus> (V (Suc (Suc 0)))))), ((((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc 0))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc 0))))) \<oplus> (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc 0)))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc 0))))) \<oplus> (((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc 0))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc 0))) \<ominus> (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc 0))))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc 0)))))))) \<odot> (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc 0)))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc 0)))))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), 
((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc 0)))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT 0))), ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc 0))))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> (C (NAT (Suc 0)))), ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))), (Ty ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) \<oplus> (C (NAT (Suc 0)))) vtype.Nat), ((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))) \<preceq> ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) \<oplus> (C (NAT (Suc 0))))), 
(Ty (Old (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) vtype.Nat), (((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) \<oplus> (C (NAT (Suc 0)))) \<doteq> (Old ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<oplus> (C (NAT (Suc 0)))))), ((IF (Old (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) \<oplus> (C (NAT (Suc 0)))) ELSE (IF (Old (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) \<doteq> (C (NAT (Suc (Suc (Suc 0))))) THEN ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc 0))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc 0))))) \<oplus> (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc 0)))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc 0))))) ELSE (IF (Old (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) \<doteq> (C (NAT (Suc 0))) THEN ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> 
(C (NAT (Suc 0))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc 0))) \<ominus> (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc 0))))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc 0)))))))) ELSE (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (Old (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (Deref (Old (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))) \<doteq> Rp), ((((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) \<oplus> (C (NAT (Suc 0)))) \<oplus> ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc 0))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc 0))) \<ominus> (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc 0))))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc 0))))))))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), 
(\<Prod>0. ((\<Lambda> [(Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc 0))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc 0))))))), (((Lv 0) \<oplus> (C (NAT (Suc 0)))) \<prec> ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) \<oplus> (C (NAT (Suc 0)))))]) \<supset> ((IF (Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) \<oplus> (C (NAT (Suc 0)))) ELSE (IF (Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc 0))))) THEN ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc 0))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc 0))))) \<oplus> (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc 0)))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc 0))))) ELSE (IF (Lv 0) \<doteq> (C (NAT (Suc 0))) THEN ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc 0))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc 0))) \<ominus> (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc 0))))))) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc 0)))))))) ELSE (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (Lv 0) THEN (Deref (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (Deref (Lv 0)))))) \<doteq> (Old (Deref (Lv 0))))))])]))]))]))]))]))]), 
(\<Lambda> [((\<Lambda> [(\<Lambda> [T, (\<Lambda> [(Ty (V (Suc 0)) vtype.Nat), (Ty (V (Suc (Suc 0))) vtype.Nat), (Ty (V (Suc (Suc (Suc 0)))) vtype.Nat), (Ty (Old (V (Suc 0))) vtype.Nat), (Ty (Old (V (Suc (Suc 0)))) vtype.Nat), (Ty (Old (V (Suc (Suc (Suc 0))))) vtype.Nat), ((C (NAT 0)) \<prec> (Old (V (Suc 0)))), ((V (Suc 0)) \<doteq> (Old ((V (Suc 0)) \<ominus> (C (NAT (Suc 0)))))), ((V (Suc (Suc 0))) \<doteq> (Old (V (Suc (Suc 0))))), ((V (Suc (Suc (Suc 0)))) \<doteq> (Old ((V (Suc (Suc (Suc 0)))) \<oplus> (V (Suc (Suc 0)))))), (((V (Suc (Suc (Suc 0)))) \<oplus> ((V (Suc 0)) \<odot> (V (Suc (Suc 0))))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), ((V (Suc (Suc (Suc (Suc 0))))) \<doteq> (C (NAT 0))), ((V (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc 0)))), ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))), (Ty (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) vtype.Nat), ((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))) \<preceq> (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))), (Ty (Old (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) vtype.Nat), ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (Old ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<oplus> (C (NAT (Suc 0)))))), 
((Deref (Old (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))) \<doteq> Rp), (((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<oplus> (V (Suc 0))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), (\<Prod>0. ((\<Lambda> [(Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc 0))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc 0))))))), (((Lv 0) \<oplus> (C (NAT (Suc 0)))) \<prec> (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))]) \<supset> ((Deref (Lv 0)) \<doteq> (Old (Deref (Lv 0))))))])]), (Pc \<doteq> (C (POS ((Suc 0), (Suc (Suc (Suc (Suc (Suc 0)))))))))]) \<supset> (\<Lambda> [(\<Lambda> [(Ty (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) vtype.Nat), (Ty (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) vtype.Nat)]), (\<Lambda> [(Ty (V (Suc 0)) vtype.Nat), (Ty (V (Suc (Suc 0))) vtype.Nat), (Ty (V (Suc (Suc (Suc 0)))) vtype.Nat), (((V (Suc (Suc (Suc 0)))) \<oplus> ((V (Suc 0)) \<odot> (V (Suc (Suc 0))))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), ((V (Suc (Suc (Suc (Suc 0))))) \<doteq> (C (NAT 0))), ((V (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc 0)))), ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))), (Ty (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) vtype.Nat), ((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))) \<preceq> (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))), (((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<oplus> (V (Suc 0))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), ((C (POS ((Suc 0), (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (POS ((Suc 0), 
(Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))), (\<Prod>0. ((Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) \<supset> ((IF (Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) THEN (C (POS ((Suc 0), (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (Deref (Lv 0))) \<doteq> (Deref (Lv 0)))))])]))]), (\<Lambda> [((\<Lambda> [(\<Lambda> [(\<Lambda> [(Ty (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) vtype.Nat), (Ty (V (Suc (Suc (Suc (Suc (Suc 0)))))) vtype.Nat)]), (\<Lambda> [(Ty (V (Suc (Suc (Suc 0)))) vtype.Nat), (Ty (Old (V (Suc (Suc (Suc 0))))) vtype.Nat), (Ty (Old (V (Suc 0))) vtype.Nat), (Ty (Old (V (Suc (Suc 0)))) vtype.Nat), ((V (Suc (Suc (Suc 0)))) \<doteq> (Old ((V (Suc (Suc (Suc 0)))) \<oplus> ((V (Suc 0)) \<odot> (V (Suc (Suc 0))))))), ((V (Suc (Suc (Suc (Suc 0))))) \<doteq> (C (NAT 0))), ((V (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc 0)))), ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))), (Ty (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) vtype.Nat), ((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))) \<preceq> (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))), (Ty (Old (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) vtype.Nat), 
((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (Old ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<oplus> (C (NAT (Suc 0)))))), ((Deref (Old (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))) \<doteq> Rp), (((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<oplus> (V (Suc 0))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), (\<Prod>0. ((\<Lambda> [(Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc 0))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc 0))))))), (((Lv 0) \<oplus> (C (NAT (Suc 0)))) \<prec> (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))]) \<supset> ((Deref (Lv 0)) \<doteq> (Old (Deref (Lv 0))))))])]), (Pc \<doteq> (C (POS ((Suc 0), (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))]) \<supset> (\<Lambda> [(\<Lambda> [(Ty ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) vtype.Nat), (Ty (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) vtype.Nat)]), (((C (POS ((Suc 0), (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) \<doteq> (C (POS ((Suc 0), 
(Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))) \<supset> (\<Lambda> [(\<Lambda> [((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) THEN (IF ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) ELSE (Deref ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> Rp), (Ty (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) THEN (IF ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) ELSE (Deref ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) Pos)]), 
(\<Lambda> [(Ty (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (C (NAT (Suc (Suc (Suc 0))))) THEN (IF ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) ELSE (Deref ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc 0))))) vtype.Nat), (Ty (Old (V (Suc (Suc (Suc 0))))) vtype.Nat), (Ty (Old (V (Suc 0))) vtype.Nat), (Ty (Old (V (Suc (Suc 0)))) vtype.Nat), ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (C (NAT (Suc (Suc (Suc 0))))) THEN (IF ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) ELSE (Deref ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc 0))))) \<doteq> (Old ((V (Suc (Suc (Suc 0)))) \<oplus> ((V (Suc 0)) \<odot> (V (Suc (Suc 0))))))), ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc 0)))))) THEN (IF 
((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) ELSE (Deref ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT 0))), ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc 0))))))) THEN (IF ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) ELSE (Deref ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> (C (NAT (Suc 0)))), ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) THEN (IF ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> 
(V (Suc (Suc (Suc (Suc (Suc 0))))))) ELSE (Deref ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))), ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) THEN (IF ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) ELSE (Deref ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> Rp), (Ty (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN 
(IF ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) ELSE (Deref ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0)))))))) vtype.Nat), ((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))) \<preceq> (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN (IF ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) ELSE (Deref ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))))), 
(((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN (IF ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) ELSE (Deref ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0)))))))) \<oplus> (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (C (NAT (Suc 0))) THEN (IF ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) ELSE (Deref ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (V (Suc 0)))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), 
((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN (IF ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) ELSE (Deref ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (Old (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))), (\<Prod>0. ((\<Lambda> [(Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc 0))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc 0))))))), ((Lv 0) \<prec> (IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN (IF ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> 
(C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) ELSE (Deref ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0)))))))))]) \<supset> ((IF (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (Lv 0) THEN (IF ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) ELSE (Deref ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))))) ELSE (IF (Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) THEN ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<ominus> (V (Suc (Suc (Suc (Suc (Suc 0))))))) ELSE (Deref (Lv 0)))) \<doteq> (Old (Deref (Lv 0))))))])]))]))]), (\<Lambda> [((\<Lambda> [(\<Lambda> [(\<Lambda> [((V (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> Rp), 
(Ty (V (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) Pos)]), (\<Lambda> [(Ty (V (Suc (Suc (Suc 0)))) vtype.Nat), (Ty (Old (V (Suc (Suc (Suc 0))))) vtype.Nat), (Ty (Old (V (Suc 0))) vtype.Nat), (Ty (Old (V (Suc (Suc 0)))) vtype.Nat), ((V (Suc (Suc (Suc 0)))) \<doteq> (Old ((V (Suc (Suc (Suc 0)))) \<oplus> ((V (Suc 0)) \<odot> (V (Suc (Suc 0))))))), ((V (Suc (Suc (Suc (Suc 0))))) \<doteq> (C (NAT 0))), ((V (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc 0)))), ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))), ((V (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> Rp), (Ty (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) vtype.Nat), ((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))) \<preceq> (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))), (((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<oplus> (V (Suc 0))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (Old (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))), (\<Prod>0. ((\<Lambda> [(Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))), 
(Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc 0))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc 0))))))), ((Lv 0) \<prec> (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))]) \<supset> ((Deref (Lv 0)) \<doteq> (Old (Deref (Lv 0))))))])]), (\<Lambda> [((V (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> (C (POS (0, (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))), (Pc \<doteq> (C (POS ((Suc 0), (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))), (\<Lambda> [((Old (V (Suc 0))) \<doteq> (Old (C (NAT (Suc (Suc 0)))))), ((Old (V (Suc (Suc 0)))) \<doteq> (Old (C (NAT (Suc (Suc (Suc 0))))))), ((Old (V (Suc (Suc (Suc 0))))) \<doteq> (Old (C (NAT 0)))), ((Old (V (Suc (Suc (Suc (Suc 0)))))) \<doteq> (Old (C (NAT 0)))), ((Old (V (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> (Old (C (NAT (Suc 0))))), ((Old (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (Old (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))), ((Old (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) \<doteq> (Old (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))), (\<Prod>0. ((\<Lambda> [(Neg ((Old (Lv 0)) \<doteq> (Old (C (NAT (Suc 0)))))), (Neg ((Old (Lv 0)) \<doteq> (Old (C (NAT (Suc (Suc 0))))))), (Neg ((Old (Lv 0)) \<doteq> (Old (C (NAT (Suc (Suc (Suc 0)))))))), 
(Neg ((Old (Lv 0)) \<doteq> (Old (C (NAT (Suc (Suc (Suc (Suc 0))))))))), (Neg ((Old (Lv 0)) \<doteq> (Old (C (NAT (Suc (Suc (Suc (Suc (Suc 0)))))))))), (Neg ((Old (Lv 0)) \<doteq> (Old (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))), (Neg ((Old (Lv 0)) \<doteq> (Old (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))]) \<supset> ((Old (Deref (Lv 0))) \<doteq> (Old (Old (Deref (Lv 0)))))))])])]) \<supset> (\<Lambda> [T, ((V (Suc (Suc (Suc 0)))) \<doteq> ((C (NAT (Suc (Suc 0)))) \<odot> (C (NAT (Suc (Suc (Suc 0)))))))])), ((\<Lambda> [(\<Lambda> [(\<Lambda> [((V (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> Rp), (Ty (V (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) Pos)]), (\<Lambda> [(Ty (V (Suc (Suc (Suc 0)))) vtype.Nat), (Ty (Old (V (Suc (Suc (Suc 0))))) vtype.Nat), (Ty (Old (V (Suc 0))) vtype.Nat), (Ty (Old (V (Suc (Suc 0)))) vtype.Nat), ((V (Suc (Suc (Suc 0)))) \<doteq> (Old ((V (Suc (Suc (Suc 0)))) \<oplus> ((V (Suc 0)) \<odot> (V (Suc (Suc 0))))))), ((V (Suc (Suc (Suc (Suc 0))))) \<doteq> (C (NAT 0))), ((V (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc 0)))), ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))), ((V (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> Rp), (Ty (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) vtype.Nat), ((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))) \<preceq> (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))), 
(((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<oplus> (V (Suc 0))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (Old (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))), (\<Prod>0. ((\<Lambda> [(Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc 0))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc 0))))))), ((Lv 0) \<prec> (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))]) \<supset> ((Deref (Lv 0)) \<doteq> (Old (Deref (Lv 0))))))])]), (\<Lambda> [((V (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> (C (POS ((Suc 0), (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))), (Pc \<doteq> (C (POS ((Suc 0), (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))), (\<Lambda> [(Ty (Old (V (Suc 0))) vtype.Nat), (Ty (Old (V (Suc (Suc 0)))) vtype.Nat), (Ty (Old (V (Suc (Suc (Suc 0))))) vtype.Nat), (Ty (Old (Old (V (Suc 0)))) vtype.Nat), (Ty (Old (Old (V (Suc (Suc 0))))) vtype.Nat), (Ty (Old (Old (V (Suc (Suc (Suc 0)))))) vtype.Nat), ((Old (C (NAT 0))) \<prec> (Old (Old (V (Suc 0))))), ((Old (V (Suc 0))) \<doteq> (Old (Old ((V (Suc 0)) \<ominus> (C (NAT (Suc 0))))))), ((Old (V (Suc (Suc 0)))) \<doteq> (Old (Old (V (Suc (Suc 0)))))), 
((Old (V (Suc (Suc (Suc 0))))) \<doteq> (Old (Old ((V (Suc (Suc (Suc 0)))) \<oplus> (V (Suc (Suc 0))))))), ((Old ((V (Suc (Suc (Suc 0)))) \<oplus> ((V (Suc 0)) \<odot> (V (Suc (Suc 0)))))) \<preceq> (Old (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))))), ((Old (V (Suc (Suc (Suc (Suc 0)))))) \<doteq> (Old (C (NAT 0)))), ((Old (V (Suc (Suc (Suc (Suc (Suc 0))))))) \<doteq> (Old (C (NAT (Suc 0))))), ((Old (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (Old (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))), (Ty (Old (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) vtype.Nat), ((Old (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))) \<preceq> (Old (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))), (Ty (Old (Old (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))) vtype.Nat), ((Old (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))) \<doteq> (Old (Old ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<oplus> (C (NAT (Suc 0))))))), ((Old (Deref (Old (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))) \<doteq> (Old Rp)), ((Old ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<oplus> (V (Suc 0)))) \<preceq> (Old (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))))))))), 
(\<Prod>0. ((\<Lambda> [(Neg ((Old (Lv 0)) \<doteq> (Old (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))), (Neg ((Old (Lv 0)) \<doteq> (Old (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))))), (Neg ((Old (Lv 0)) \<doteq> (Old (C (NAT (Suc 0)))))), (Neg ((Old (Lv 0)) \<doteq> (Old (C (NAT (Suc (Suc (Suc 0)))))))), ((Old ((Lv 0) \<oplus> (C (NAT (Suc 0))))) \<prec> (Old (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))]) \<supset> ((Old (Deref (Lv 0))) \<doteq> (Old (Old (Deref (Lv 0)))))))])])]) \<supset> (\<Lambda> [(\<Lambda> [(Ty (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) vtype.Nat), (Ty (V (Suc (Suc (Suc (Suc (Suc 0)))))) vtype.Nat)]), (\<Lambda> [(Ty (V (Suc (Suc (Suc 0)))) vtype.Nat), (Ty (Old (Old (V (Suc (Suc (Suc 0)))))) vtype.Nat), (Ty (Old (Old (V (Suc 0)))) vtype.Nat), (Ty (Old (Old (V (Suc (Suc 0))))) vtype.Nat), ((V (Suc (Suc (Suc 0)))) \<doteq> (Old (Old ((V (Suc (Suc (Suc 0)))) \<oplus> ((V (Suc 0)) \<odot> (V (Suc (Suc 0)))))))), ((V (Suc (Suc (Suc (Suc 0))))) \<doteq> (C (NAT 0))), ((V (Suc (Suc (Suc (Suc (Suc 0)))))) \<doteq> (C (NAT (Suc 0)))), ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))), 
(Ty (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) vtype.Nat), ((C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))) \<preceq> (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))), (Ty (Old (Old (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))) vtype.Nat), ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<doteq> (Old (Old ((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<oplus> (C (NAT (Suc 0))))))), ((Deref (Old (Old (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))) \<doteq> (Old Rp)), (((V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))) \<oplus> (V (Suc 0))) \<preceq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))))))))), (\<Prod>0. ((\<Lambda> [(Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc 0))))), (Neg ((Lv 0) \<doteq> (C (NAT (Suc (Suc (Suc 0))))))), (((Lv 0) \<oplus> (C (NAT (Suc 0)))) \<prec> (V (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))))]) \<supset> ((Deref (Lv 0)) \<doteq> (Old (Old (Deref (Lv 0)))))))])]))])])"

subsection {* Verifying the program *}

(*<*)
lemma lambda_split_pairs:
"(\<lambda> (s::(nat \<times> nat) \<times> (nat \<Rightarrow> tval) \<times> \<lparr>cs :: (nat \<times> (nat \<Rightarrow> tval)) list, h :: (nat \<times> nat) list\<rparr>). (P s)) = (\<lambda> (pc,m,e). (P (pc,m,e)))"
apply simp
done

lemma domC_prog:"domC prog = [(0,0),(0,1),(0,2),(0,3),(0,4),(0,5),(0,6),(0,7),(0,8),(1,0),(1,1),(1,2),(1,3),(1,4),(1,5),(1,6),(1,7),(1,8)]"
apply (simp add: domC.simps prog_def Let_def fst_conv snd_conv)
done

lemma anF_prog:"domA prog = [(0,7),(0,8),(1,0),(1,5),(1,6),(1,8)]"
apply (simp only: domA_def domC_prog)
apply (simp add: anF.simps prog_def noProc.simps Let_def fst_conv snd_conv split_def filter.simps)
done
lemma disjE2: "a | b \<Longrightarrow> ~ a \<Longrightarrow> b"
apply auto
done

lemma env_simp:
"e\<lparr>h:=a,h:=b\<rparr> = e\<lparr>h:=b\<rparr>"
apply simp
done

lemma suc_eq_plus1:
"Suc x = x + 1"
apply simp
done

lemma conjI':
"\<lbrakk> X; X \<Longrightarrow> Y \<rbrakk> \<Longrightarrow> (X \<and> Y)"
by blast
(*>*)

text {* First we ensure that the program is wellformed. *}

lemma wf_prog:
"wf prog"
apply (simp add: wf_def domC_prog checkPos.simps prog_def Let_def split_def
fst_conv snd_conv cmd.simps ret_succs.simps callpoints_def isCall_def anF.simps)
done

(*<*)
lemma less_diff_conv2: "((a::nat) + b < c) = (a < c - b)"
apply arith
done

--{* Lemmas about validity of formulae *}
lemma validF_True: "validF I s T = True" 
by simp

lemma validF_False: "validF I s F = False" 
by simp

lemma validF_And_Nil: "validF I s (\<Lambda> []) = True" 
by simp

lemma validF_And_Cons: "validF I s (\<Lambda> (f # fs)) = ((validF I s f) \<and> (validF I s (\<Lambda> fs)))"
by simp

lemma validF_And_Cons_Nil: "validF I s (\<Lambda> [f]) = (validF I s f)"
by simp 


lemma validF_Imp: "validF I s (f1 \<supset> f2) = ((validF I s f1) \<longrightarrow> (validF I s f2))" 
by simp

lemma validF_Neg: "validF I s (Neg f) = (\<not> (validF I s f))" 
by simp

lemma validF_Eq: "validF I s (e1 \<doteq> e2) = ((eval I s e1) = (eval I s e2))" 
by simp

lemma validF_Leq: "validF I s (e1 \<preceq> e2) = ((nv (eval I s e1)) \<le> (nv (eval I s e2)))" 
by simp

lemma validF_Less: "validF I s (e1 \<prec> e2) = ((nv (eval I s e1)) < (nv (eval I s e2)))" 
by simp

lemma validF_Forall: "validF I s (\<Prod>v. f) = (\<forall>tv. (validF (I[v::=tv]) s f))"
by (simp add: Let_def)
(*>*)

text {* Establish System Invariants *}

lemma vc_proof_startup:
"\<And> s. \<lbrakk> wf prg; s \<in> isafeP prg \<rbrakk> \<Longrightarrow> sysinv (s,prg) \<and> sysinv2 (s,prg) \<and> (\<exists> c css. cs (snd (snd s)) = c#css)"
(*<*)
apply (rule context_conjI)
 apply (rule sysinv_pres')
 apply assumption
 apply assumption
apply (rule context_conjI)
 apply (cut_tac sysinv2_pres)
 apply (erule_tac x="prg" in allE)
 apply (erule_tac x="s" in allE)
 apply (drule mp, assumption)+
 apply assumption
apply (case_tac "cs (snd (snd s))")
apply (simp add: sysinv.simps split_paired_all)
apply (rule_tac x="a" in exI)
apply (rule_tac x="list" in exI)
apply (case_tac "list")
apply (simp add: sysinv.simps Let_def split_def fst_conv snd_conv split_paired_all)
apply fastsimp
(*>*)
done


text {* Then, we prove the verification condition *}

lemma nat_mult_mono:
"0 < (n::nat) \<Longrightarrow> x \<le> n * x"
apply (induct n)
apply simp
apply simp
done

lemma vc_prog_holds:
"provable prog vc"
apply (simp only: provable_def valid_def split_paired_all | rule HOLprf | rule ballI | rule allI | rule impI)+
apply (rename_tac "pn" "i" "m" "e" "I")
apply (cut_tac wf_prog, drule vc_proof_startup,assumption, (erule conjE | erule exE)+, (simp only: fst_conv snd_conv))

--{* Now, the prelude is finished. The main proof starts . . . *}
apply (simp only: vc_def)
(* txt {* \newpage @{subgoals [display, indent=0, margin=100]} *} *)

apply (case_tac "prog,((pn,i),m,e) \<Turnstile> (initF prog)")
apply (simp add: initF_def valid_def form.cases validF_validFs.simps nv_def Let_def split_def fst_conv snd_conv id_lookup_def FiniteMap.del_def)


--{* not initF prog *}


--{* startzustand *}
apply (subst validF_Imp)
apply (rule impI)
apply (subst validF_And_Cons)
apply (rule conjI)
apply (simp add: valid_def validF_validFs.simps initF_def Let_def split_def fst_conv snd_conv nv_def FiniteMap.del_def update_def)
apply (rule impI)
apply (erule conjE | erule exE)+
apply (case_tac "css")
apply simp

apply (rule allI)
apply simp

apply (subst validF_And_Cons)
apply (rule conjI)
-- {* (0,7) - - > (1,0) *}
apply (simp add: validF_validFs.simps form.cases Let_def split_def fst_conv snd_conv lift_def nv_def FiniteMap.del_def)

apply (subst validF_And_Cons)
apply (rule conjI)
--{* (0,8) - - > (0,8) *}
apply (simp add: validF_validFs.simps form.cases Let_def split_def fst_conv snd_conv  lift_def nv_def)

apply ( subst validF_And_Cons)
apply (rule conjI)
--{* (1,0) - - > (1,5) *}
apply (simp only: validF_And_Cons validF_Imp)
apply (rule conjI)
apply (rule impI)
apply (simp add: validF_validFs.simps form.cases Let_def split_def fst_conv snd_conv lift_def nv_def FiniteMap.del_def)
apply (erule conjE)+
apply (case_tac "css")
apply simp

--{* css = a list *}
apply (subgoal_tac "(\<exists> n8. m 8 = NAT n8) \<and>  (\<exists> n3. m 3 = NAT n3) \<and>  (\<exists> n2. m 2 = NAT n2) \<and> (\<exists> n1. m 1 = NAT n1)")
 prefer 2
 apply (rule conjI)
 apply (case_tac "m 8")
 apply (simp add: nat_number)
 apply (simp add: nat_number)
 apply (simp add: nat_number)
 
 apply (rule conjI)
 apply (case_tac "m 3")
 apply (simp add: nat_number)
 apply (simp add: nat_number)
 apply (simp add: nat_number)
 
 apply (rule conjI)
 apply (case_tac "m 2")
 apply (simp add: nat_number)
 apply (simp add: nat_number)
 apply (simp add: nat_number)

 apply (case_tac "m 1")
 apply (simp add: nat_number)
 apply (simp add: nat_number)
 apply (simp add: nat_number)
apply (subgoal_tac "fst (snd (callstate e)) 1 = m 1") 
 prefer 2
 apply (erule_tac x="NAT 1" in allE)
 apply (simp add: nat_number update_def  Let_def split_def fst_conv snd_conv id_lookup_def)
apply (subgoal_tac "fst (snd (callstate e)) 2 = m 2") 
 prefer 2
 apply (erule_tac x="NAT 2" in allE)
 apply (simp add: nat_number update_def Let_def split_def fst_conv snd_conv id_lookup_def)
apply (subgoal_tac "fst (snd (callstate e)) 3 = m 3") 
 prefer 2
 apply (erule_tac x="NAT 3" in allE)
 apply (simp add: nat_number update_def Let_def split_def fst_conv snd_conv id_lookup_def)
apply (subgoal_tac "fst (snd (callstate e)) 8 = m 8") 
 prefer 2
 apply (erule_tac x="NAT 8" in allE)
 apply (simp add: nat_number update_def Let_def split_def fst_conv snd_conv id_lookup_def)
apply (erule conjE | erule exE)+ 
apply (simp add: nat_number update_def Let_def id_lookup_def)
apply (rule conjI)
apply (rule impI)
apply (rule allI)
apply (erule_tac x="tv" in allE)
apply (rule impI)
apply (erule conjE)+
apply (case_tac "tv")
apply (simp add: nat_number update_def Let_def)

apply (simp add: nat_number update_def Let_def)

apply (simp add: nat_number update_def Let_def)


apply (rule impI)
apply (rule conjI)
apply (subgoal_tac "n2 \<le> n1 * n2")
 prefer 2
 apply (rule nat_mult_mono)
 apply assumption
apply arith

apply (rule conjI)
apply (simp add: diff_mult_distrib)

apply (rule conjI)
apply (simp add: split_def fst_conv snd_conv Let_def)

apply (rule allI)
apply (erule_tac x="tv" in allE)
apply (rule impI)
apply (erule conjE)+
apply (case_tac "tv")
apply (simp add: nat_number update_def Let_def)

apply (simp add: nat_number update_def Let_def id_lookup_def)

apply (simp add: nat_number update_def Let_def)

apply (simp add: validF_validFs.simps)

apply (subst validF_And_Cons)
apply (rule conjI)
--{* (1,5) nach (1,0) *}
apply (simp only: update_def nat_number validF_validFs.simps  map.simps form.cases Let_def split_def fst_conv snd_conv lift_def nv_def id_lookup_def eval.simps simp_thms)
apply (rule impI)
apply (erule conjE)+
apply (case_tac "css")
apply simp

--{* css = a list *}
apply (subgoal_tac "(\<exists> n8. m 8 = NAT n8) \<and>  (\<exists> n3. m 3 = NAT n3) \<and>  (\<exists> n2. m 2 = NAT n2) \<and> (\<exists> n1. m 1 = NAT n1)")
 prefer 2
 apply (rule conjI)
 apply (case_tac "m 8")
 apply (simp add: nat_number)
 apply (rule_tac x="nat" in exI)
 apply assumption
 apply (erule_tac V="m (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))) = ?P" in thin_rl)
 apply (simp add: nat_number tval.cases)
 
 apply (rule conjI)
 apply (case_tac "m 3")
 apply (simp add: nat_number) 
 apply (rule_tac x="nat" in exI)
 apply assumption
 apply (erule_tac V="m (Suc (Suc (Suc 0))) = ?P" in thin_rl)
 apply (simp add: nat_number)
 
 apply (rule conjI)
 apply (case_tac "m 2")
 apply (simp add: nat_number) 
 apply (rule_tac x="nat" in exI)
 apply assumption
 apply (erule_tac V="m (Suc (Suc 0)) = ?P" in thin_rl)
 apply (simp add: nat_number)

 apply (case_tac "m 1")
 apply (simp add: nat_number) 
 apply (rule_tac x="nat" in exI)
 apply assumption
 apply (erule_tac V="m (Suc 0) = ?P" in thin_rl)
 apply (simp add: nat_number)

apply (erule conjE | erule exE)+ 
apply (simp add: nat_number update_def Let_def id_lookup_def)

apply (subst validF_And_Cons)
apply (rule conjI)
--{* (1,6) nach (1,8) *}
apply (simp only: validF_validFs.simps map.simps form.cases Let_def split_def fst_conv snd_conv lift_def nv_def id_lookup_def eval.simps simp_thms tval.cases)
apply (rule impI)
apply (case_tac "css")
apply (simp add: Let_def)
--{* case css = a list *}
apply (erule conjE | erule exE)+
apply (simp add: Let_def)
apply (rule context_conjI)
--{* Wenn S=Soff=9, dann s'a=8, dann m 8 = NAT und m 8 = POS .. Typkonflikt *}
apply (case_tac "fst (snd (callstate e)) (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))")
apply (simp add: nat_number)
apply (simp add: nat_number)
apply (simp add: nat_number)


apply (case_tac "fst (snd (callstate e)) (Suc 0)")
apply (simp add: MAX_def nat_number)
prefer 2
apply (simp add: nat_number MAX_def)
apply (simp add: nat_number MAX_def)

apply (case_tac "fst (snd (callstate e)) (Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0))))))))")
apply (simp add: nat_number)
prefer 2
apply (simp add: nat_number)
apply (simp add: nat_number)

apply (case_tac "nata = Suc (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))))")
apply (simp add: nat_number)
apply (simp add: nat_number)

apply (case_tac "m (Suc 0)")
apply (simp add: MAX_def nat_number)
prefer 2
apply (simp add: nat_number MAX_def)
apply (simp add: nat_number MAX_def)

apply (rule allI)
apply (case_tac tv)
apply (simp add: nat_number update_def Let_def id_lookup_def)

prefer 2
apply (simp add: nat_number update_def Let_def id_lookup_def)

apply (simp add: nat_number update_def Let_def id_lookup_def)
apply (rule impI)
apply (erule conjE)+
apply (erule_tac x="NAT natc" in allE)
apply (simp add: lift_def Let_def nv_def nat_number update_def)

apply (subst validF_And_Cons_Nil)
--{* (1,8) nach (0,8) *}
apply (simp only: nat_number update_def validF_validFs.simps map.simps form.cases Let_def split_def fst_conv snd_conv lift_def id_lookup_def eval.simps simp_thms)
apply (rule conjI)
apply (rule impI)
apply (erule conjE)+
apply simp

apply (rule impI)
apply (erule conjE)+
apply (simp add: nv_def)
apply (rule conjI)
apply (erule conjE)+
apply (case_tac "fst (snd (callstate (snd (snd (callstate e))))) 3")
apply (simp add: nat_number)

prefer 2
apply (simp add: nat_number)

apply (simp add: nat_number)
apply (case_tac "fst (snd (callstate (snd (snd (callstate e))))) 2")
apply (simp add: nat_number)

prefer 2
apply (simp add: nat_number)

apply (simp add: nat_number)
apply (case_tac "fst (snd (callstate (snd (snd (callstate e))))) (Suc 0)")
apply (simp add: nat_number)

prefer 2
apply (simp add: nat_number)

apply (simp add: diff_mult_distrib nat_number)

apply (rule conjI)
apply (erule conjE)+
apply (case_tac "fst (snd (callstate (snd (snd (callstate e))))) 8")
apply (simp add: nat_number)

prefer 2
apply (simp add: nat_number)
apply (simp add: nat_number)
apply (erule_tac x="NAT nat" in allE)
apply (simp add: nat_number id_lookup_def Let_def)
apply (case_tac "css")
apply (simp add: id_lookup_def Let_def)
apply (simp add: callstate_def Let_def split_def fst_conv snd_conv id_lookup_def)
apply (case_tac "nat = 8")
apply (simp add: nat_number)

apply (simp add: nat_number)

apply (rule allI)
apply (simp add: nat_number id_lookup_def Let_def lift_def)
apply (case_tac tv)
apply simp
prefer 2
apply simp
apply (erule_tac x="tv" in allE)
apply (erule_tac x="tv" in allE)
apply (simp add: id_lookup_def Let_def)
apply (rule impI)
apply (erule conjE)+
apply (simp add: split_def Let_def)
done

end