Theory FNF_F_sf_rest

Up to index of Isabelle/HOL/HOL-Complex/CSP/CSP_T/CSP_F/FNF_F

theory FNF_F_sf_rest
imports FNF_F_sf_def
begin
           (*-------------------------------------------*
            |        CSP-Prover on Isabelle2005         |
            |              Februaru 2006                |
            |                                           |
            |        Yoshinao Isobe (AIST JAPAN)        |
            *-------------------------------------------*)

theory FNF_F_sf_rest = FNF_F_sf_def:

(*  The following simplification rules are deleted in this theory file *)
(*  because they unexpectly rewrite UnionT and InterT.                 *)
(*                  disj_not1: (~ P | Q) = (P --> Q)                   *)

declare disj_not1 [simp del]

(*  The following simplification rules are deleted in this theory file *)
(*       P (if Q then x else y) = ((Q --> P x) & (~ Q --> P y))        *)

declare split_if  [split del]

(*****************************************************************

         1. full sequentialization for Depth-restriction (P |. n)
         2.
         3.

 *****************************************************************)

(*============================================================*
 |                                                            |
 |                       Depth_rest                           |
 |                                                            |
 *============================================================*)

(*============================================================*
 |                         Pfun P1 P2                         |
 *============================================================*)

(*** relation ***)

consts
  fsfF_Depth_rest_rel ::
  "('a proc * nat * 'a proc) set"

  fsfF_Depth_rest ::
  "'a proc => nat => 'a proc"   ("(1_ /|.seq _)" [84,900] 84)

inductive 
  "fsfF_Depth_rest_rel"

intros
fsfF_Depth_rest_rel_zero:
  "(P1, 0, SDIV) : fsfF_Depth_rest_rel"

fsfF_Depth_rest_rel_etc:
  "P1 ~: fsfF_proc
   ==> (P1, Suc n, P1 |. (Suc n)) : fsfF_Depth_rest_rel"

fsfF_Depth_rest_rel_int:
  "[| ALL c. if (c:C1)
             then (Rf1 c, Suc n, SRf c) : fsfF_Depth_rest_rel
             else SRf c = DIV ;
      C1 ~= {} ; ALL c:C1. Rf1 c : fsfF_proc |]
   ==>
   ((!! :C1 .. Rf1), Suc n, !! c:C1 .. SRf c)
   : fsfF_Depth_rest_rel"

fsfF_Depth_rest_rel_step:
  "[| ALL a. if a:A1
             then (Pf1 a, n, SPf a) : fsfF_Depth_rest_rel
             else SPf a = DIV ;
      ALL a:A1. Pf1 a : fsfF_proc ;
      Q1 = SKIP | Q1 = DIV | Q1 = STOP |]
   ==> 
   ((? :A1 -> Pf1) [+] Q1, Suc n, (? :A1 -> SPf) [+] Q1) : fsfF_Depth_rest_rel"

(*** function ***)

defs
  fsfF_Depth_rest_def:
    "P1 |.seq n == THE SP. (P1, n, SP) : fsfF_Depth_rest_rel"

(****************************************************************
 |                      uniquness                               |
 ****************************************************************)

lemma fsfF_Depth_rest_rel_unique_in_lm:
   "(P1, n, SP1) : fsfF_Depth_rest_rel
    ==> (ALL SP2. ((P1, n, SP2) : fsfF_Depth_rest_rel
                   --> SP1 = SP2))"
apply (rule fsfF_Depth_rest_rel.induct[of P1 n SP1])
apply (simp)

(* zero *)
apply (intro allI impI)
apply (rotate_tac -1)
apply (erule fsfF_Depth_rest_rel.elims)
apply (simp_all)

(* etc *)
apply (intro allI impI)
apply (rotate_tac -1)
apply (erule fsfF_Depth_rest_rel.elims)
apply (simp_all)
apply (simp add: fsfF_proc_int)
apply (simp add: fsfF_proc_ext)

(* step_int *)
apply (intro allI impI)
apply (rotate_tac -1)
apply (erule fsfF_Depth_rest_rel.elims, simp_all)

 apply (elim conjE exE)
 apply (rotate_tac -3)
 apply (drule sym)
 apply (simp add: fsfF_proc_int)

 apply (simp add: expand_fun_eq)
 apply (intro allI)
 apply (drule_tac x="x" in spec)+
 apply (case_tac "x : C1a")
 apply (simp)
 apply (simp)

(* step *)
apply (intro allI impI)
apply (rotate_tac -1)
apply (erule fsfF_Depth_rest_rel.elims, simp_all)

 apply (elim conjE exE)
 apply (rotate_tac -3)
 apply (drule sym)
 apply (simp add: fsfF_proc_ext)

  apply (simp add: expand_fun_eq)
  apply (rule allI)
  apply (drule_tac x="x" in spec)+
  apply (case_tac "x : A1a")
  apply (simp_all)
done

(*-----------------------*
 |        unique         |
 *-----------------------*)

lemma fsfF_Depth_rest_rel_unique:
   "[| (P1, n, SP1) : fsfF_Depth_rest_rel;
       (P1, n, SP2) : fsfF_Depth_rest_rel |]
    ==> SP1 = SP2"
by (simp add: fsfF_Depth_rest_rel_unique_in_lm)

lemma fsfF_Depth_rest_rel_EX1:
   "(EX SP. (P1, n, SP) : fsfF_Depth_rest_rel)
 = (EX! SP. (P1, n, SP) : fsfF_Depth_rest_rel)"
apply (rule iffI)

 apply (erule exE)
 apply (rule_tac a="SP" in ex1I)
 apply (simp)
 apply (simp add: fsfF_Depth_rest_rel_unique)

 apply (elim ex1_implies_exE)
 apply (simp)
done

(*------------------------------------------------------------*
 |                   fsfF_Depth_rest_rel (iff)                |
 *------------------------------------------------------------*)

(* zero *)

lemma fsfF_Depth_rest_rel_zero_iff:
  "(P1, 0, SP) : fsfF_Depth_rest_rel
   = (SP = SDIV)"
apply (rule)
apply (erule fsfF_Depth_rest_rel.elims, simp_all)
apply (simp add: fsfF_Depth_rest_rel_zero)
done

(* etc *)

lemma fsfF_Depth_rest_rel_etc_iff:
  "P1 ~: fsfF_proc
   ==> (P1, Suc n, SP) : fsfF_Depth_rest_rel
       = (SP = P1 |. Suc n)"
apply (rule)
apply (erule fsfF_Depth_rest_rel.elims, simp_all)
 apply (simp add: fsfF_proc_int)
 apply (simp add: fsfF_proc_ext)
apply (simp add: fsfF_Depth_rest_rel_etc)
done

(* int *)

lemma fsfF_Depth_rest_rel_int_iff:
  "[| ALL c. if (c:C1)
             then (Rf1 c, Suc n, SRf c) : fsfF_Depth_rest_rel
             else SRf c = DIV ;
      C1 ~= {} ; ALL c:C1. Rf1 c : fsfF_proc |]
   ==>
   ((!! :C1 .. Rf1), Suc n, SP) : fsfF_Depth_rest_rel
   = (SP = !! :C1 .. SRf)"
apply (rule)
apply (erule fsfF_Depth_rest_rel.elims, simp_all)
 apply (elim conjE)
 apply (rotate_tac -3)
 apply (drule sym)
 apply (simp add: fsfF_proc_int)

 apply (simp add: expand_fun_eq)
 apply (rule allI)
 apply (drule_tac x="x" in spec)+
 apply (case_tac "x : C1a")
 apply (simp add: fsfF_Depth_rest_rel_unique)

 apply (simp)
apply (simp add: fsfF_Depth_rest_rel_int)
done

(* step *)

lemma fsfF_Depth_rest_rel_step_iff:
  "[| ALL a. if a:A1
             then (Pf1 a, n, SPf a) : fsfF_Depth_rest_rel
             else SPf a = DIV ;
      ALL a:A1. Pf1 a : fsfF_proc ;
      Q1 = SKIP | Q1 = DIV | Q1 = STOP |]
   ==> 
   ((? :A1 -> Pf1) [+] Q1, Suc n, SP) : fsfF_Depth_rest_rel
   = (SP = (? :A1 -> SPf) [+] Q1)"
apply (rule)
apply (erule fsfF_Depth_rest_rel.elims, simp_all)
 apply (elim conjE)
 apply (rotate_tac -3)
 apply (drule sym)
 apply (simp add: fsfF_proc_ext)

 apply (simp add: expand_fun_eq)
 apply (intro allI conjI)
 apply (elim conjE)
 apply (drule_tac x="x" in spec)+
 apply (case_tac "x : A1a")
 apply (simp add: fsfF_Depth_rest_rel_unique)
 apply (simp)
apply (simp add: fsfF_Depth_rest_rel_step)
done

(****************************************************************
 |                      existency                               |
 ****************************************************************)

(*** exists ***)

lemma fsfF_Depth_rest_rel_exists_zero:
   "(EX SP. (P1, 0, SP) : fsfF_Depth_rest_rel)"
apply (rule_tac x="SDIV" in exI)
apply (simp add: fsfF_Depth_rest_rel.intros)
done

lemma fsfF_Depth_rest_rel_exists_notin:
   "P1 ~: fsfF_proc
    ==> (EX SP. (P1, n, SP) : fsfF_Depth_rest_rel)"
apply (insert nat_zero_or_Suc)
apply (drule_tac x="n" in spec)
apply (elim disjE exE)
apply (simp add: fsfF_Depth_rest_rel_exists_zero)
apply (rule_tac x="P1 |. n" in exI)
apply (simp add: fsfF_Depth_rest_rel.intros)
done

(*** in fsfF_proc ***)

(********* P1 and P2 *********)

lemma fsfF_Depth_rest_rel_exists_in:
   "P1 : fsfF_proc
    ==> ALL n. (EX SP. (P1, n, SP) :  fsfF_Depth_rest_rel)"
apply (rule fsfF_proc.induct[of P1])
apply (simp)

(* int *)
apply (rule allI)
apply (insert nat_zero_or_Suc)
apply (drule_tac x="n" in spec)
apply (elim disjE exE)
apply (simp add: fsfF_Depth_rest_rel_exists_zero)

apply (erule dist_BALL_conjE)
apply (simp add: exchange_ALL_BALL)
apply (simp add: choice_BALL_EX)
apply (drule_tac x="n" in spec)
apply (elim exE)
apply (rule_tac x="!! c:C .. (if (c : C) then f c else DIV)" in exI)
apply (rule fsfF_Depth_rest_rel.intros)
apply (simp split: split_if)
apply (simp_all)

(* ext *)
apply (rule allI)
apply (drule_tac x="n" in spec)
apply (rotate_tac -1)
apply (erule disjE)
apply (simp add: fsfF_Depth_rest_rel_exists_zero)

apply (elim exE)
apply (erule dist_BALL_conjE)

apply (simp add: exchange_ALL_BALL)
apply (simp add: choice_BALL_EX)
apply (drule_tac x="m" in spec)
apply (elim exE)
apply (rule_tac x="? a:A -> (if (a : A) then (f a) else DIV) [+] Q" in exI)
apply (rule fsfF_Depth_rest_rel.intros)
apply (simp split: split_if)
apply (simp_all)
done

(*-----------------------*
 |        exists         |
 *-----------------------*)

lemma fsfF_Depth_rest_rel_exists:
   "EX SP. (P1, n, SP) :  fsfF_Depth_rest_rel"
apply (case_tac "P1 ~: fsfF_proc")
apply (simp add: fsfF_Depth_rest_rel_exists_notin)
apply (simp add: fsfF_Depth_rest_rel_exists_in)
done

(*-----------------------*
 |    uniquely exists    |
 *-----------------------*)

lemma fsfF_Depth_rest_rel_unique_exists:
   "EX! SP. (P1, n, SP) :  fsfF_Depth_rest_rel"
apply (simp add: fsfF_Depth_rest_rel_EX1[THEN sym])
apply (simp add: fsfF_Depth_rest_rel_exists)
done

(*------------------------------------------------------------*
 |                        in fsfF_proc                        |
 *------------------------------------------------------------*)

lemma fsfF_Depth_rest_rel_zero_in:
  "(P1, 0, SP) : fsfF_Depth_rest_rel ==> SP : fsfF_proc"
apply (simp add: fsfF_Depth_rest_rel_zero_iff)
done

lemma fsfF_Depth_rest_rel_in_lm:
  "P1 : fsfF_proc ==> 
   ALL n SP. (P1, n, SP) : fsfF_Depth_rest_rel --> SP : fsfF_proc"
apply (rule fsfF_proc.induct[of P1])
apply (simp)

(* int *)
apply (intro allI)
apply (insert nat_zero_or_Suc)
apply (drule_tac x="n" in spec)
apply (elim disjE exE)
apply (simp add: fsfF_Depth_rest_rel_zero_in)

apply (intro impI)
apply (simp)
apply (rotate_tac -1)
apply (erule fsfF_Depth_rest_rel.elims, simp_all)
 apply (elim conjE)
 apply (rotate_tac -3)
 apply (drule sym)
 apply (simp add: fsfF_proc.intros)

apply (rule fsfF_proc.intros)
apply (simp_all)
apply (rule ballI)
apply (drule_tac x="c" in spec)
apply (drule_tac x="c" in bspec, simp)
apply (force)

(* ext *)
apply (intro allI)
apply (drule_tac x="n" in spec)
apply (rotate_tac -1)
apply (erule disjE)
apply (simp add: fsfF_Depth_rest_rel_zero_in)

apply (intro impI)
apply (erule fsfF_Depth_rest_rel.elims, simp_all)
 apply (elim conjE)
 apply (rotate_tac -3)
 apply (drule sym)
 apply (simp add: fsfF_proc.intros)

apply (rule fsfF_proc.intros)
apply (simp_all)
apply (rule ballI)
apply (drule_tac x="a" in spec)
apply (drule_tac x="a" in bspec, simp)
apply (force)
done

(*------------------------------------*
 |                 in                 |
 *------------------------------------*)

lemma fsfF_Depth_rest_rel_in:
  "[| P1 : fsfF_proc ; (P1, n, SP) : fsfF_Depth_rest_rel |]
   ==> SP : fsfF_proc"
apply (insert fsfF_Depth_rest_rel_in_lm[of P1])
apply (blast)
done

(*------------------------------------------------------------*
 |             syntactical transformation to fsfF             |
 *------------------------------------------------------------*)

(*** relation ***)

lemma cspF_fsfF_Depth_rest_rel_eqF_zero:
   "(P1, 0, SP) : fsfF_Depth_rest_rel
     ==> P1 |. 0 =F SP"
apply (simp add: fsfF_Depth_rest_rel_zero_iff)
apply (rule cspF_rw_left)
apply (rule cspF_Depth_rest_Zero)
apply (rule cspF_SDIV_eqF)
done

lemma cspF_fsfF_Depth_rest_rel_eqF_notin:
   "[| P1 ~: fsfF_proc ; (P1, n, SP) : fsfF_Depth_rest_rel |]
    ==> P1 |. n =F SP"
apply (insert nat_zero_or_Suc)
apply (drule_tac x="n" in spec)
apply (elim disjE exE)
apply (simp add: cspF_fsfF_Depth_rest_rel_eqF_zero)
apply (simp add: fsfF_Depth_rest_rel_etc_iff)
done

lemma cspF_fsfF_Depth_rest_rel_eqF_in:
    "P1 : fsfF_proc ==>
     ALL n SP. (P1, n, SP) : fsfF_Depth_rest_rel
                --> P1 |. n =F SP"
apply (rule fsfF_proc.induct[of P1])
apply (simp)

(* int *)
apply (intro allI)
apply (insert nat_zero_or_Suc)
apply (drule_tac x="n" in spec)
apply (elim disjE exE)
apply (simp add: cspF_fsfF_Depth_rest_rel_eqF_zero)

apply (intro impI)
apply (simp)
apply (rotate_tac -1)
apply (erule fsfF_Depth_rest_rel.elims, simp_all)
apply (elim conjE)

apply (rule cspF_rw_left)
apply (rule cspF_Dist)
apply (rule cspF_decompo)
apply (simp)
apply (drule_tac x="c" in bspec, simp)
apply (drule_tac x="c" in spec)
apply (simp)

(* ext *)
apply (intro allI)
apply (drule_tac x="n" in spec)
apply (rotate_tac -1)
apply (erule disjE)
apply (simp add: cspF_fsfF_Depth_rest_rel_eqF_zero)

apply (intro impI)
apply (erule fsfF_Depth_rest_rel.elims, simp_all)

apply (rule cspF_rw_left)
apply (rule cspF_Ext_dist)
apply (rule cspF_decompo)

 apply (rule cspF_rw_left)
 apply (rule cspF_step)
 apply (rule cspF_decompo)
 apply (simp)
 apply (simp)
 apply (case_tac "Q = STOP")
 apply (simp add: cspF_STOP_Depth_rest)
 apply (simp add: cspF_SKIP_or_DIV_Depth_rest)
done

(*------------------------------------*
 |                 eqF                |
 *------------------------------------*)

lemma cspF_fsfF_Depth_rest_rel_eqF:
   "(P1, n, SP) : fsfF_Depth_rest_rel ==> P1 |. n =F SP"
apply (case_tac "P1 ~: fsfF_proc")
apply (simp add: cspF_fsfF_Depth_rest_rel_eqF_notin)
apply (simp add: cspF_fsfF_Depth_rest_rel_eqF_in)
done

(*************************************************************
                  relation --> function
 *************************************************************)

lemma fsfF_Depth_rest_in_rel:
    "(P1, n, P1 |.seq n) : fsfF_Depth_rest_rel"
apply (simp add: fsfF_Depth_rest_def)
apply (rule theI'
  [of "(%R. (P1, n, R) : fsfF_Depth_rest_rel)"])
apply (simp add: fsfF_Depth_rest_rel_unique_exists)
done

lemma fsfF_Depth_rest_from_rel:
    "((P1, n, SP) : fsfF_Depth_rest_rel)
   = (P1 |.seq n = SP)"
apply (rule iffI)
apply (simp add: fsfF_Depth_rest_def)
apply (simp add: fsfF_Depth_rest_rel_unique_exists the1_equality)

apply (drule sym)
apply (simp add: fsfF_Depth_rest_in_rel)
done

lemma fsfF_Depth_rest_to_rel:
    "(P1 |.seq n = SP)
   = ((P1, n, SP) : fsfF_Depth_rest_rel)"
by (simp add: fsfF_Depth_rest_from_rel)

(*************************************************************
                          function
 *************************************************************)

lemma fsfF_Depth_rest_zero:
  "P1 |.seq 0 = SDIV"
apply (simp add: fsfF_Depth_rest_to_rel)
apply (simp add: fsfF_Depth_rest_rel_zero_iff)
done

lemma fsfF_Depth_rest_etc:
  "P1 ~: fsfF_proc
   ==> P1 |.seq (Suc n) = P1 |. (Suc n)"
apply (simp add: fsfF_Depth_rest_to_rel)
apply (simp add: fsfF_Depth_rest_rel_etc_iff)
done

lemma fsfF_Depth_rest_int:
  "[| C1 ~= {} ; ALL c:C1. Rf1 c : fsfF_proc |]
   ==>
   (!! :C1 .. Rf1) |.seq (Suc n) = 
    !! c:C1 .. (if c:C1 then (Rf1 c |.seq (Suc n)) else DIV)"
apply (simp add: fsfF_Depth_rest_to_rel)
apply (rule fsfF_Depth_rest_rel_int)
apply (simp_all)
apply (simp split: split_if)
apply (simp add: fsfF_Depth_rest_in_rel)
done

lemma fsfF_Depth_rest_step:
  "[| ALL a:A1. Pf1 a : fsfF_proc ; Q1 = SKIP | Q1 = DIV | Q1 = STOP |]
   ==>
    ((? :A1 -> Pf1) [+] Q1) |.seq (Suc n) = 
    ((? a:A1 -> (if (a:A1) then (Pf1 a |.seq n) else DIV)) [+] Q1)"
apply (simp add: fsfF_Depth_rest_to_rel)
apply (rule fsfF_Depth_rest_rel_step)
apply (simp_all)
apply (simp split: split_if)
apply (simp add: fsfF_Depth_rest_in_rel)
done

lemmas fsfF_Depth_rest =
       fsfF_Depth_rest_etc
       fsfF_Depth_rest_int
       fsfF_Depth_rest_step

(*------------------------------------------------------------*
 |                        in fsfF_proc                        |
 *------------------------------------------------------------*)

lemma fsfF_Depth_rest_in:
  "P1 : fsfF_proc
   ==> P1 |.seq n : fsfF_proc"
apply (rule fsfF_Depth_rest_rel_in[of P1 n])
apply (simp_all add: fsfF_Depth_rest_in_rel)
done

(*------------------------------------------------------------*
 |             syntactical transformation to fsfF             |
 *------------------------------------------------------------*)

lemma cspF_fsfF_Depth_rest_eqF:
   "P1 |. n =F P1 |.seq n"
apply (rule cspF_fsfF_Depth_rest_rel_eqF)
apply (simp add: fsfF_Depth_rest_in_rel)
done

(****************** to add them again ******************)

declare split_if    [split]
declare disj_not1   [simp]

end

lemma fsfF_Depth_rest_rel_unique_in_lm: 

  (P1.0, n, SP1.0) ∈ fsfF_Depth_rest_rel
  ==> ∀SP2. (P1.0, n, SP2) ∈ fsfF_Depth_rest_rel --> SP1.0 = SP2

lemma fsfF_Depth_rest_rel_unique: 

  [| (P1.0, n, SP1.0) ∈ fsfF_Depth_rest_rel;
     (P1.0, n, SP2.0) ∈ fsfF_Depth_rest_rel |]
  ==> SP1.0 = SP2.0

lemma fsfF_Depth_rest_rel_EX1: 

  (∃SP. (P1.0, n, SP) ∈ fsfF_Depth_rest_rel) =
  (∃!SP. (P1.0, n, SP) ∈ fsfF_Depth_rest_rel)

lemma fsfF_Depth_rest_rel_zero_iff: 

  ((P1.0, 0, SP) ∈ fsfF_Depth_rest_rel) = (SP = SDIV)

lemma fsfF_Depth_rest_rel_etc_iff: 

  P1.0 ∉ fsfF_proc
  ==> ((P1.0, Suc n, SP) ∈ fsfF_Depth_rest_rel) = (SP = P1.0 |. Suc n)

lemma fsfF_Depth_rest_rel_int_iff: 

  [| ∀c. if c ∈ C1.0 then (Rf1.0 c, Suc n, SRf c) ∈ fsfF_Depth_rest_rel
         else SRf c = DIV;
     C1.0 ≠ {}; ∀c∈C1.0. Rf1.0 c ∈ fsfF_proc |]
  ==> ((!! :C1.0 .. Rf1.0, Suc n, SP) ∈ fsfF_Depth_rest_rel) =
      (SP = !! :C1.0 .. SRf)

lemma fsfF_Depth_rest_rel_step_iff: 

  [| ∀a. if a ∈ A1.0 then (Pf1.0 a, n, SPf a) ∈ fsfF_Depth_rest_rel
         else SPf a = DIV;
     ∀a∈A1.0. Pf1.0 a ∈ fsfF_proc; Q1.0 = SKIP ∨ Q1.0 = DIV ∨ Q1.0 = STOP |]
  ==> ((? :A1.0 -> Pf1.0 [+] Q1.0, Suc n, SP) ∈ fsfF_Depth_rest_rel) =
      (SP = ? :A1.0 -> SPf [+] Q1.0)

lemma fsfF_Depth_rest_rel_exists_zero: 

  ∃SP. (P1.0, 0, SP) ∈ fsfF_Depth_rest_rel

lemma fsfF_Depth_rest_rel_exists_notin: 

  P1.0 ∉ fsfF_proc ==> ∃SP. (P1.0, n, SP) ∈ fsfF_Depth_rest_rel

lemma fsfF_Depth_rest_rel_exists_in: 

  P1.0 ∈ fsfF_proc ==> ∀n. ∃SP. (P1.0, n, SP) ∈ fsfF_Depth_rest_rel

lemma fsfF_Depth_rest_rel_exists: 

  ∃SP. (P1.0, n, SP) ∈ fsfF_Depth_rest_rel

lemma fsfF_Depth_rest_rel_unique_exists: 

  ∃!SP. (P1.0, n, SP) ∈ fsfF_Depth_rest_rel

lemma fsfF_Depth_rest_rel_zero_in: 

  (P1.0, 0, SP) ∈ fsfF_Depth_rest_rel ==> SP ∈ fsfF_proc

lemma fsfF_Depth_rest_rel_in_lm: 

  P1.0 ∈ fsfF_proc
  ==> ∀n SP. (P1.0, n, SP) ∈ fsfF_Depth_rest_rel --> SP ∈ fsfF_proc

lemma fsfF_Depth_rest_rel_in: 

  [| P1.0 ∈ fsfF_proc; (P1.0, n, SP) ∈ fsfF_Depth_rest_rel |] ==> SP ∈ fsfF_proc

lemma cspF_fsfF_Depth_rest_rel_eqF_zero: 

  (P1.0, 0, SP) ∈ fsfF_Depth_rest_rel ==> P1.0 |. 0 =F SP

lemma cspF_fsfF_Depth_rest_rel_eqF_notin: 

  [| P1.0 ∉ fsfF_proc; (P1.0, n, SP) ∈ fsfF_Depth_rest_rel |] ==> P1.0 |. n =F SP

lemma cspF_fsfF_Depth_rest_rel_eqF_in: 

  P1.0 ∈ fsfF_proc
  ==> ∀n SP. (P1.0, n, SP) ∈ fsfF_Depth_rest_rel --> P1.0 |. n =F SP

lemma cspF_fsfF_Depth_rest_rel_eqF: 

  (P1.0, n, SP) ∈ fsfF_Depth_rest_rel ==> P1.0 |. n =F SP

lemma fsfF_Depth_rest_in_rel: 

  (P1.0, n, P1.0 |.seq n) ∈ fsfF_Depth_rest_rel

lemma fsfF_Depth_rest_from_rel: 

  ((P1.0, n, SP) ∈ fsfF_Depth_rest_rel) = (P1.0 |.seq n = SP)

lemma fsfF_Depth_rest_to_rel: 

  (P1.0 |.seq n = SP) = ((P1.0, n, SP) ∈ fsfF_Depth_rest_rel)

lemma fsfF_Depth_rest_zero: 

  P1.0 |.seq 0 = SDIV

lemma fsfF_Depth_rest_etc: 

  P1.0 ∉ fsfF_proc ==> P1.0 |.seq Suc n = P1.0 |. Suc n

lemma fsfF_Depth_rest_int: 

  [| C1.0 ≠ {}; ∀c∈C1.0. Rf1.0 c ∈ fsfF_proc |]
  ==> (!! :C1.0 .. Rf1.0) |.seq Suc n =
      !! c:C1.0 .. (if c ∈ C1.0 then Rf1.0 c |.seq Suc n else DIV)

lemma fsfF_Depth_rest_step: 

  [| ∀a∈A1.0. Pf1.0 a ∈ fsfF_proc; Q1.0 = SKIP ∨ Q1.0 = DIV ∨ Q1.0 = STOP |]
  ==> (? :A1.0 -> Pf1.0 [+] Q1.0) |.seq Suc n =
      ? a:A1.0 -> (if a ∈ A1.0 then Pf1.0 a |.seq n else DIV) [+] Q1.0

lemmas fsfF_Depth_rest: 

  P1.0 ∉ fsfF_proc ==> P1.0 |.seq Suc n = P1.0 |. Suc n
  [| C1.0 ≠ {}; ∀c∈C1.0. Rf1.0 c ∈ fsfF_proc |]
  ==> (!! :C1.0 .. Rf1.0) |.seq Suc n =
      !! c:C1.0 .. (if c ∈ C1.0 then Rf1.0 c |.seq Suc n else DIV)
  [| ∀a∈A1.0. Pf1.0 a ∈ fsfF_proc; Q1.0 = SKIP ∨ Q1.0 = DIV ∨ Q1.0 = STOP |]
  ==> (? :A1.0 -> Pf1.0 [+] Q1.0) |.seq Suc n =
      ? a:A1.0 -> (if a ∈ A1.0 then Pf1.0 a |.seq n else DIV) [+] Q1.0

lemmas fsfF_Depth_rest: 

  P1.0 ∉ fsfF_proc ==> P1.0 |.seq Suc n = P1.0 |. Suc n
  [| C1.0 ≠ {}; ∀c∈C1.0. Rf1.0 c ∈ fsfF_proc |]
  ==> (!! :C1.0 .. Rf1.0) |.seq Suc n =
      !! c:C1.0 .. (if c ∈ C1.0 then Rf1.0 c |.seq Suc n else DIV)
  [| ∀a∈A1.0. Pf1.0 a ∈ fsfF_proc; Q1.0 = SKIP ∨ Q1.0 = DIV ∨ Q1.0 = STOP |]
  ==> (? :A1.0 -> Pf1.0 [+] Q1.0) |.seq Suc n =
      ? a:A1.0 -> (if a ∈ A1.0 then Pf1.0 a |.seq n else DIV) [+] Q1.0

lemma fsfF_Depth_rest_in: 

  P1.0 ∈ fsfF_proc ==> P1.0 |.seq n ∈ fsfF_proc

lemma cspF_fsfF_Depth_rest_eqF: 

  P1.0 |. n =F P1.0 |.seq n