Definition: treeco
treeco(E) ==  corec(X.lbl:Atom × if lbl =a "leaf" then E if lbl =a "node" then left:X × X else Void fi )
Lemma: treeco_wf
∀[E:Type]. (treeco(E) ∈ Type)
Lemma: treeco-ext
∀[E:Type]. treeco(E) ≡ lbl:Atom × if lbl =a "leaf" then E if lbl =a "node" then left:treeco(E) × treeco(E) else Void fi 
Definition: treeco_size
treeco_size(p) ==
  fix((λsize,p. let lbl,x = p 
                in if lbl =a "leaf" then 0
                   if lbl =a "node" then let left,right = x in (1 + (size left)) + (size right)
                   else 0
                   fi )) 
  p
Lemma: treeco_size_wf
∀[E:Type]. ∀[p:treeco(E)].  (treeco_size(p) ∈ partial(ℕ))
Definition: tree
tree(E) ==  {p:treeco(E)| (treeco_size(p))↓} 
Lemma: tree_wf
∀[E:Type]. (tree(E) ∈ Type)
Definition: tree_size
tree_size(p) ==
  fix((λsize,p. let lbl,x = p 
                in if lbl =a "leaf" then 0
                   if lbl =a "node" then let left,right = x in (1 + (size left)) + (size right)
                   else 0
                   fi )) 
  p
Lemma: tree_size_wf
∀[E:Type]. ∀[p:tree(E)].  (tree_size(p) ∈ ℕ)
Lemma: tree-ext
∀[E:Type]. tree(E) ≡ lbl:Atom × if lbl =a "leaf" then E if lbl =a "node" then left:tree(E) × tree(E) else Void fi 
Definition: tree_leaf
tree_leaf(value) ==  <"leaf", value>
Lemma: tree_leaf_wf
∀[E:Type]. ∀[value:E].  (tree_leaf(value) ∈ tree(E))
Definition: tree_node
tree_node(left;right) ==  <"node", left, right>
Lemma: tree_node_wf
∀[E:Type]. ∀[left,right:tree(E)].  (tree_node(left;right) ∈ tree(E))
Definition: tree_leaf?
tree_leaf?(v) ==  fst(v) =a "leaf"
Lemma: tree_leaf?_wf
∀[E:Type]. ∀[v:tree(E)].  (tree_leaf?(v) ∈ 𝔹)
Definition: tree_leaf-value
tree_leaf-value(v) ==  snd(v)
Lemma: tree_leaf-value_wf
∀[E:Type]. ∀[v:tree(E)].  tree_leaf-value(v) ∈ E supposing ↑tree_leaf?(v)
Definition: tree_node?
tree_node?(v) ==  fst(v) =a "node"
Lemma: tree_node?_wf
∀[E:Type]. ∀[v:tree(E)].  (tree_node?(v) ∈ 𝔹)
Definition: tree_node-left
tree_node-left(v) ==  fst(snd(v))
Lemma: tree_node-left_wf
∀[E:Type]. ∀[v:tree(E)].  tree_node-left(v) ∈ tree(E) supposing ↑tree_node?(v)
Definition: tree_node-right
tree_node-right(v) ==  snd(snd(v))
Lemma: tree_node-right_wf
∀[E:Type]. ∀[v:tree(E)].  tree_node-right(v) ∈ tree(E) supposing ↑tree_node?(v)
Lemma: tree-induction
∀[E:Type]. ∀[P:tree(E) ⟶ ℙ].
  ((∀value:E. P[tree_leaf(value)])
  
⇒ (∀left,right:tree(E).  (P[left] 
⇒ P[right] 
⇒ P[tree_node(left;right)]))
  
⇒ {∀v:tree(E). P[v]})
Lemma: tree-definition
∀[E,A:Type]. ∀[R:A ⟶ tree(E) ⟶ ℙ].
  ((∀value:E. {x:A| R[x;tree_leaf(value)]} )
  
⇒ (∀left,right:tree(E).  ({x:A| R[x;left]}  
⇒ {x:A| R[x;right]}  
⇒ {x:A| R[x;tree_node(left;right)]} ))
  
⇒ {∀v:tree(E). {x:A| R[x;v]} })
Definition: tree_ind
tree_ind(v;
         tree_leaf(value)
⇒ leaf[value];
         tree_node(left,right)
⇒ rec1,rec2.node[left;
                                                right;
                                                rec1;
                                                rec2])  ==
  fix((λtree_ind,v. let lbl,v1 = v 
                    in if lbl="leaf" then leaf[v1]
                       if lbl="node"
                         then let left,v2 = v1 
                              in node[left;
                                      v2;
                                      tree_ind left;
                                      tree_ind v2]
                       else Ax
                       fi )) 
  v
Lemma: tree_ind_wf
∀[E,A:Type]. ∀[R:A ⟶ tree(E) ⟶ ℙ]. ∀[v:tree(E)]. ∀[leaf:value:E ⟶ {x:A| R[x;tree_leaf(value)]} ].
∀[node:left:tree(E) ⟶ right:tree(E) ⟶ {x:A| R[x;left]}  ⟶ {x:A| R[x;right]}  ⟶ {x:A| R[x;tree_node(left;right)]} ].
  (tree_ind(v;
            tree_leaf(value)
⇒ leaf[value];
            tree_node(left,right)
⇒ rec1,rec2.node[left;right;rec1;rec2])  ∈ {x:A| R[x;v]} )
Lemma: tree_ind_wf_simple
∀[E,A:Type]. ∀[v:tree(E)]. ∀[leaf:value:E ⟶ A]. ∀[node:left:tree(E) ⟶ right:tree(E) ⟶ A ⟶ A ⟶ A].
  (tree_ind(v;
            tree_leaf(value)
⇒ leaf[value];
            tree_node(left,right)
⇒ rec1,rec2.node[left;right;rec1;rec2])  ∈ A)
Lemma: tree_subtype_base
∀[E:Type]. tree(E) ⊆r Base supposing E ⊆r Base
Lemma: valuetype__tree
∀[E:Type]. value-type(tree(E))
Lemma: tree_subtype
∀[A,B:Type].  tree(A) ⊆r tree(B) supposing A ⊆r B
Definition: tree-height
tree-height(t) ==  tree_ind(t; tree_leaf(x)
⇒ 0; tree_node(l,r)
⇒ lh,rh.imax(lh;rh) + 1) 
Lemma: tree-height_wf
∀[x:Type]. ∀[t:tree(x)].  (tree-height(t) ∈ ℕ)
Comment: tree_1_end
********************************
Definition: bs_treeco
bs_treeco(E) ==
  corec(X.lbl:Atom × if lbl =a "null" then Unit
                     if lbl =a "leaf" then E
                     if lbl =a "node" then left:X × value:E × X
                     else Void
                     fi )
Lemma: bs_treeco_wf
∀[E:Type]. (bs_treeco(E) ∈ Type)
Lemma: bs_treeco-ext
∀[E:Type]
  bs_treeco(E) ≡ lbl:Atom × if lbl =a "null" then Unit
                            if lbl =a "leaf" then E
                            if lbl =a "node" then left:bs_treeco(E) × value:E × bs_treeco(E)
                            else Void
                            fi 
Definition: bs_treeco_size
bs_treeco_size(p) ==
  fix((λsize,p. let lbl,x = p 
                in if lbl =a "null" then 0
                   if lbl =a "leaf" then 0
                   if lbl =a "node" then 1 + (size (fst(x))) + (size (snd(snd(x))))
                   else 0
                   fi )) 
  p
Lemma: bs_treeco_size_wf
∀[E:Type]. ∀[p:bs_treeco(E)].  (bs_treeco_size(p) ∈ partial(ℕ))
Definition: bs_tree
bs_tree(E) ==  {p:bs_treeco(E)| (bs_treeco_size(p))↓} 
Lemma: bs_tree_wf
∀[E:Type]. (bs_tree(E) ∈ Type)
Definition: bs_tree_size
bs_tree_size(p) ==
  fix((λsize,p. let lbl,x = p 
                in if lbl =a "null" then 0
                   if lbl =a "leaf" then 0
                   if lbl =a "node" then 1 + (size (fst(x))) + (size (snd(snd(x))))
                   else 0
                   fi )) 
  p
Lemma: bs_tree_size_wf
∀[E:Type]. ∀[p:bs_tree(E)].  (bs_tree_size(p) ∈ ℕ)
Lemma: bs_tree-ext
∀[E:Type]
  bs_tree(E) ≡ lbl:Atom × if lbl =a "null" then Unit
                          if lbl =a "leaf" then E
                          if lbl =a "node" then left:bs_tree(E) × value:E × bs_tree(E)
                          else Void
                          fi 
Definition: bst_null
bst_null() ==  <"null", ⋅>
Lemma: bst_null_wf
∀[E:Type]. (bst_null() ∈ bs_tree(E))
Definition: bst_leaf
bst_leaf(value) ==  <"leaf", value>
Lemma: bst_leaf_wf
∀[E:Type]. ∀[value:E].  (bst_leaf(value) ∈ bs_tree(E))
Definition: bst_node
bst_node(left;value;right) ==  <"node", left, value, right>
Lemma: bst_node_wf
∀[E:Type]. ∀[left:bs_tree(E)]. ∀[value:E]. ∀[right:bs_tree(E)].  (bst_node(left;value;right) ∈ bs_tree(E))
Definition: bst_null?
bst_null?(v) ==  fst(v) =a "null"
Lemma: bst_null?_wf
∀[E:Type]. ∀[v:bs_tree(E)].  (bst_null?(v) ∈ 𝔹)
Definition: bst_leaf?
bst_leaf?(v) ==  fst(v) =a "leaf"
Lemma: bst_leaf?_wf
∀[E:Type]. ∀[v:bs_tree(E)].  (bst_leaf?(v) ∈ 𝔹)
Definition: bst_leaf-value
bst_leaf-value(v) ==  snd(v)
Lemma: bst_leaf-value_wf
∀[E:Type]. ∀[v:bs_tree(E)].  bst_leaf-value(v) ∈ E supposing ↑bst_leaf?(v)
Definition: bst_node?
bst_node?(v) ==  fst(v) =a "node"
Lemma: bst_node?_wf
∀[E:Type]. ∀[v:bs_tree(E)].  (bst_node?(v) ∈ 𝔹)
Definition: bst_node-left
bst_node-left(v) ==  fst(snd(v))
Lemma: bst_node-left_wf
∀[E:Type]. ∀[v:bs_tree(E)].  bst_node-left(v) ∈ bs_tree(E) supposing ↑bst_node?(v)
Definition: bst_node-value
bst_node-value(v) ==  fst(snd(snd(v)))
Lemma: bst_node-value_wf
∀[E:Type]. ∀[v:bs_tree(E)].  bst_node-value(v) ∈ E supposing ↑bst_node?(v)
Definition: bst_node-right
bst_node-right(v) ==  snd(snd(snd(v)))
Lemma: bst_node-right_wf
∀[E:Type]. ∀[v:bs_tree(E)].  bst_node-right(v) ∈ bs_tree(E) supposing ↑bst_node?(v)
Lemma: bs_tree-induction
∀[E:Type]. ∀[P:bs_tree(E) ⟶ ℙ].
  (P[bst_null()]
  
⇒ (∀value:E. P[bst_leaf(value)])
  
⇒ (∀left:bs_tree(E). ∀value:E. ∀right:bs_tree(E).  (P[left] 
⇒ P[right] 
⇒ P[bst_node(left;value;right)]))
  
⇒ {∀v:bs_tree(E). P[v]})
Lemma: bs_tree-definition
∀[E,A:Type]. ∀[R:A ⟶ bs_tree(E) ⟶ ℙ].
  ({x:A| R[x;bst_null()]} 
  
⇒ (∀value:E. {x:A| R[x;bst_leaf(value)]} )
  
⇒ (∀left:bs_tree(E). ∀value:E. ∀right:bs_tree(E).
        ({x:A| R[x;left]}  
⇒ {x:A| R[x;right]}  
⇒ {x:A| R[x;bst_node(left;value;right)]} ))
  
⇒ {∀v:bs_tree(E). {x:A| R[x;v]} })
Definition: bs_tree_ind
case(v)
null=>null
leaf(value)=>leaf[value]
node(left,value,right)=>rec1,rec2.node[left;
                                       value;
                                       right;
                                       rec1;
                                       rec2] ==
  fix((λbs_tree_ind,v. let lbl,v1 = v 
                       in if lbl="null" then null
                          if lbl="leaf" then leaf[v1]
                          if lbl="node"
                            then let left,v2 = v1 
                                 in let value,v3 = v2 
                                    in node[left;
                                            value;
                                            v3;
                                            bs_tree_ind left;
                                            bs_tree_ind v3]
                          else Ax
                          fi )) 
  v
Lemma: bs_tree_ind_wf
∀[E,A:Type]. ∀[R:A ⟶ bs_tree(E) ⟶ ℙ]. ∀[v:bs_tree(E)]. ∀[null:{x:A| R[x;bst_null()]} ].
∀[leaf:value:E ⟶ {x:A| R[x;bst_leaf(value)]} ]. ∀[node:left:bs_tree(E)
                                                       ⟶ value:E
                                                       ⟶ right:bs_tree(E)
                                                       ⟶ {x:A| R[x;left]} 
                                                       ⟶ {x:A| R[x;right]} 
                                                       ⟶ {x:A| R[x;bst_node(left;value;right)]} ].
  (case(v)
   null=>null
   leaf(value)=>leaf[value]
   node(left,value,right)=>rec1,rec2.node[left;value;right;rec1;rec2] ∈ {x:A| R[x;v]} )
Lemma: bs_tree_ind_wf_simple
∀[E,A:Type]. ∀[v:bs_tree(E)]. ∀[null:A]. ∀[leaf:value:E ⟶ A]. ∀[node:left:bs_tree(E)
                                                                      ⟶ value:E
                                                                      ⟶ right:bs_tree(E)
                                                                      ⟶ A
                                                                      ⟶ A
                                                                      ⟶ A].
  (case(v)
   null=>null
   leaf(value)=>leaf[value]
   node(left,value,right)=>rec1,rec2.node[left;value;right;rec1;rec2] ∈ A)
Definition: member_bs_tree
x ∈ tr ==  case(tr)null=>Falseleaf(v)=>v = x ∈ Enode(a,v,b)=>mema,memb.(v = x ∈ E) ∨ mema ∨ memb
Lemma: member_bs_tree_wf
∀[E:Type]. ∀[x:E]. ∀[tr:bs_tree(E)].  (x ∈ tr ∈ ℙ)
Definition: bs_tree_ordered
bs_tree_ordered(E;cmp;tr) ==
  case(tr)
  null=>True
  leaf(v)=>True
  node(a,v,b)=>oa,ob.oa ∧ ob ∧ (∀x:E. (x ∈ a 
⇒ 0 < cmp x v)) ∧ (∀x:E. (x ∈ b 
⇒ 0 < cmp v x))
Lemma: bs_tree_ordered_wf
∀[E:Type]. ∀[cmp:comparison(E)]. ∀[tr:bs_tree(E)].  (bs_tree_ordered(E;cmp;tr) ∈ ℙ)
Lemma: sq_stable__bs_tree_ordered
∀[E:Type]. ∀cmp:comparison(E). ∀tr:bs_tree(E).  SqStable(bs_tree_ordered(E;cmp;tr))
Definition: ordered_bs_tree
ordered_bs_tree(E;cmp) ==  {tr:bs_tree(E)| bs_tree_ordered(E;cmp;tr)} 
Lemma: ordered_bs_tree_wf
∀[E:Type]. ∀[cmp:comparison(E)].  (ordered_bs_tree(E;cmp) ∈ Type)
Definition: bs_tree_insert
bs_tree_insert(cmp;x;tr) ==
  case(tr)
  null=>bst_leaf(x)
  leaf(v)=>eval c = cmp v x in
           if (0) < (c)
              then bst_node(bst_leaf(v);x;bst_null())
              else if (c) < (0)  then bst_node(bst_null();x;bst_leaf(v))  else bst_leaf(x)
  node(l,v,r)=>a,b.eval c = cmp v x in
                   if (0) < (c)  then bst_node(l;v;b)  else if (c) < (0)  then bst_node(a;v;r)  else bst_node(l;x;r)
Lemma: bs_tree_insert_wf1
∀[E:Type]. ∀[cmp:comparison(E)]. ∀[x:E]. ∀[tr:bs_tree(E)].  (bs_tree_insert(cmp;x;tr) ∈ bs_tree(E))
Lemma: member_bs_tree_insert
∀[E:Type]
  ∀cmp:comparison(E). ∀x:E. ∀tr:ordered_bs_tree(E;cmp). ∀y:E.
    (y ∈ bs_tree_insert(cmp;x;tr) 
⇐⇒ (y = x ∈ E) ∨ (y ∈ tr ∧ (¬((cmp x y) = 0 ∈ ℤ))))
Lemma: bs_tree_insert_wf
∀[E:Type]. ∀[cmp:comparison(E)]. ∀[x:E]. ∀[tr:ordered_bs_tree(E;cmp)].
  (bs_tree_insert(cmp;x;tr) ∈ ordered_bs_tree(E;cmp))
Definition: bs_tree_max
bs_tree_max(tr;d) ==
  case(tr)
  null=><d, bst_null()>
  leaf(v)=><v, bst_null()>
  node(a,v,b)=>ma,mb.if bst_null?(b) then <v, a> else let m,b' = mb in <m, bst_node(a;v;b')> fi 
Lemma: bs_tree_max_wf1
∀[E:Type]. ∀[tr:bs_tree(E)]. ∀[d:E].  (bs_tree_max(tr;d) ∈ E × bs_tree(E))
Lemma: member-bs_tree_max
∀[E:Type]
  ∀tr:bs_tree(E). ∀d,z:E.
    ((z ∈ snd(bs_tree_max(tr;d)) ∨ (z = (fst(bs_tree_max(tr;d))) ∈ E)) 
⇒ (z ∈ tr ∨ ((↑bst_null?(tr)) ∧ (z = d ∈ E))))
Lemma: bs_tree_max_wf
∀[E:Type]. ∀[cmp:comparison(E)]. ∀[tr:ordered_bs_tree(E;cmp)]. ∀[d:E].
  (bs_tree_max(tr;d) ∈ {p:E × ordered_bs_tree(E;cmp)| 
                        let m,t = p 
                        in (∀x:E. (x ∈ tr 
⇒ (x ∈ t ∨ (x = m ∈ E))))
                           ∧ ((¬↑bst_null?(tr)) 
⇒ m ∈ tr)
                           ∧ (∀x:E. (x ∈ t 
⇒ (x ∈ tr ∧ 0 < cmp x m)))} )
Definition: bs_tree_delete
bs_tree_delete(cmp;x;tr) ==
  case(tr)
  null=>bst_null()
  leaf(v)=>if (cmp x v =z 0) then bst_null() else bst_leaf(v) fi 
  node(a,v,b)=>da,db.if (0) < (cmp x v)
                        then bst_node(da;v;b)
                        else if (0) < (cmp v x)
                                then bst_node(a;v;db)
                                else if bst_null?(a) then b else let m,a' = bs_tree_max(a;v) in bst_node(a';m;b) fi 
Lemma: bs_tree_delete_wf1
∀[E:Type]. ∀[cmp:comparison(E)]. ∀[x:E]. ∀[tr:bs_tree(E)].  (bs_tree_delete(cmp;x;tr) ∈ bs_tree(E))
Lemma: member-bs_tree_delete-implies
∀[E:Type]. ∀cmp:comparison(E). ∀x:E. ∀tr:bs_tree(E). ∀z:E.  (z ∈ bs_tree_delete(cmp;x;tr) 
⇒ z ∈ tr)
Lemma: bs_tree_delete_wf
∀[E:Type]. ∀[cmp:comparison(E)]. ∀[x:E]. ∀[tr:ordered_bs_tree(E;cmp)].
  (bs_tree_delete(cmp;x;tr) ∈ ordered_bs_tree(E;cmp))
Lemma: sq_stable__member_bs_tree
∀[E:Type]. ∀cmp:comparison(E). ∀x:E. ∀tr:ordered_bs_tree(E;cmp).  SqStable(x ∈ tr)
Lemma: member-bs_tree_delete
∀[E:Type]
  ∀cmp:comparison(E). ∀x:E. ∀tr:ordered_bs_tree(E;cmp). ∀z:E.
    (z ∈ bs_tree_delete(cmp;x;tr) 
⇐⇒ z ∈ tr ∧ (¬((cmp z x) = 0 ∈ ℤ)))
Definition: bs_tree_lookup
bs_tree_lookup(cmp;x;tr) ==
  case(tr)
  null=>inr ⋅ 
  leaf(v)=>if (cmp v x =z 0) then inl v else inr ⋅  fi 
  node(a,v,b)=>la,lb.eval c = cmp v x in
                     if (c) < (0)  then la  else if (0) < (c)  then lb  else (inl v)
Lemma: bs_tree_lookup_wf1
∀[E:Type]. ∀[cmp:comparison(E)]. ∀[x:E]. ∀[tr:bs_tree(E)].  (bs_tree_lookup(cmp;x;tr) ∈ E?)
Lemma: bs_tree_lookup_wf
∀[E:Type]. ∀[cmp:comparison(E)]. ∀[x:E]. ∀[tr:ordered_bs_tree(E;cmp)].
  (bs_tree_lookup(cmp;x;tr) ∈ (∃z:E [(((cmp z x) = 0 ∈ ℤ) ∧ z ∈ tr)]) ∨ (↓∀z:E. (z ∈ tr 
⇒ (¬((cmp z x) = 0 ∈ ℤ)))))
Definition: test-Spec
test-Spec() ==
  [<"prog", [<"aprog", [inr Atom ]> <"iterate", [inl inl "foo"]> <"test", [inl inl "prop"]>]>
   <"foo", [<"afoo", [inr Atom ]> <"bar", [inl inl "foo"]> <"xx", [inl inl "prop"; inl inl "prog"]>]>
   <"prop", [<"aprop", [inr Atom ]> <"false", [inr Unit ]> <"implies", [inl inl "prop"; inl inl "prop"]> <"box", [inl\000C inl "prog"; inl inl "prop"]> <"diamond", [inl inl "foo"; inl inl "prop"]>]>]
Lemma: test-Spec_wf
test-Spec() ∈ MutualRectypeSpec
Definition: test-Obj
test-Obj() ==  mobj(test-Spec())
Lemma: test-Obj_wf
test-Obj() ∈ Type
Definition: test-prog
test-prog() ==  mrec(test-Spec();"prog")
Lemma: test-prog_wf
test-prog() ∈ Type
Definition: test-foo
test-foo() ==  mrec(test-Spec();"foo")
Lemma: test-foo_wf
test-foo() ∈ Type
Definition: test-prop
test-prop() ==  mrec(test-Spec();"prop")
Lemma: test-prop_wf
test-prop() ∈ Type
Definition: test-prog-obj
test-prog-obj(x) ==  <"prog", x>
Lemma: test-prog-obj_wf
∀x:test-prog(). (test-prog-obj(x) ∈ test-Obj())
Definition: test-foo-obj
test-foo-obj(x) ==  <"foo", x>
Lemma: test-foo-obj_wf
∀x:test-foo(). (test-foo-obj(x) ∈ test-Obj())
Definition: test-prop-obj
test-prop-obj(x) ==  <"prop", x>
Lemma: test-prop-obj_wf
∀x:test-prop(). (test-prop-obj(x) ∈ test-Obj())
Definition: test-aprog
test-aprog(x) ==  mk-prec("aprog";x)
Lemma: test-aprog_wf
∀[x:Atom]. (test-aprog(x) ∈ test-prog())
Definition: test-iterate
test-iterate(x) ==  mk-prec("iterate";x)
Lemma: test-iterate_wf
∀[x:test-foo()]. (test-iterate(x) ∈ test-prog())
Definition: test-test
test-test(x) ==  mk-prec("test";x)
Lemma: test-test_wf
∀[x:test-prop()]. (test-test(x) ∈ test-prog())
Definition: test-afoo
test-afoo(x) ==  mk-prec("afoo";x)
Lemma: test-afoo_wf
∀[x:Atom]. (test-afoo(x) ∈ test-foo())
Definition: test-bar
test-bar(x) ==  mk-prec("bar";x)
Lemma: test-bar_wf
∀[x:test-foo()]. (test-bar(x) ∈ test-foo())
Definition: test-xx
test-xx(x1;x) ==  mk-prec("xx";<x1, x>)
Lemma: test-xx_wf
∀[x1:test-prop()]. ∀[x:test-prog()].  (test-xx(x1;x) ∈ test-foo())
Definition: test-aprop
test-aprop(x) ==  mk-prec("aprop";x)
Lemma: test-aprop_wf
∀[x:Atom]. (test-aprop(x) ∈ test-prop())
Definition: test-false
test-false() ==  mk-prec("false";Ax)
Lemma: test-false_wf
test-false() ∈ test-prop()
Definition: test-implies
test-implies(x1;x) ==  mk-prec("implies";<x1, x>)
Lemma: test-implies_wf
∀[x1,x:test-prop()].  (test-implies(x1;x) ∈ test-prop())
Definition: test-box
test-box(x1;x) ==  mk-prec("box";<x1, x>)
Lemma: test-box_wf
∀[x1:test-prog()]. ∀[x:test-prop()].  (test-box(x1;x) ∈ test-prop())
Definition: test-diamond
test-diamond(x1;x) ==  mk-prec("diamond";<x1, x>)
Lemma: test-diamond_wf
∀[x1:test-foo()]. ∀[x:test-prop()].  (test-diamond(x1;x) ∈ test-prop())
Definition: test-kind
test-kind(d) ==  mobj-kind(d)
Lemma: test-kind_wf
∀[d:test-Obj()]. (test-kind(d) ∈ {a:Atom| (a ∈ ``prog foo prop``)} )
Definition: test-label
test-label(d) ==  mobj-label(d)
Lemma: test-label_wf
∀[d:test-Obj()]. (test-label(d) ∈ Atom)
Definition: test-aprog?
test-aprog?(x) ==  test-label(test-prog-obj(x)) =a "aprog"
Lemma: test-aprog?_wf
∀[x:test-prog()]. (test-aprog?(x) ∈ 𝔹)
Definition: test-iterate?
test-iterate?(x) ==  test-label(test-prog-obj(x)) =a "iterate"
Lemma: test-iterate?_wf
∀[x:test-prog()]. (test-iterate?(x) ∈ 𝔹)
Definition: test-test?
test-test?(x) ==  test-label(test-prog-obj(x)) =a "test"
Lemma: test-test?_wf
∀[x:test-prog()]. (test-test?(x) ∈ 𝔹)
Definition: test-afoo?
test-afoo?(x) ==  test-label(test-foo-obj(x)) =a "afoo"
Lemma: test-afoo?_wf
∀[x:test-foo()]. (test-afoo?(x) ∈ 𝔹)
Definition: test-bar?
test-bar?(x) ==  test-label(test-foo-obj(x)) =a "bar"
Lemma: test-bar?_wf
∀[x:test-foo()]. (test-bar?(x) ∈ 𝔹)
Definition: test-xx?
test-xx?(x) ==  test-label(test-foo-obj(x)) =a "xx"
Lemma: test-xx?_wf
∀[x:test-foo()]. (test-xx?(x) ∈ 𝔹)
Definition: test-aprop?
test-aprop?(x) ==  test-label(test-prop-obj(x)) =a "aprop"
Lemma: test-aprop?_wf
∀[x:test-prop()]. (test-aprop?(x) ∈ 𝔹)
Definition: test-false?
test-false?(x) ==  test-label(test-prop-obj(x)) =a "false"
Lemma: test-false?_wf
∀[x:test-prop()]. (test-false?(x) ∈ 𝔹)
Definition: test-implies?
test-implies?(x) ==  test-label(test-prop-obj(x)) =a "implies"
Lemma: test-implies?_wf
∀[x:test-prop()]. (test-implies?(x) ∈ 𝔹)
Definition: test-box?
test-box?(x) ==  test-label(test-prop-obj(x)) =a "box"
Lemma: test-box?_wf
∀[x:test-prop()]. (test-box?(x) ∈ 𝔹)
Definition: test-diamond?
test-diamond?(x) ==  test-label(test-prop-obj(x)) =a "diamond"
Lemma: test-diamond?_wf
∀[x:test-prop()]. (test-diamond?(x) ∈ 𝔹)
Definition: test-aprog-1
test-aprog-1(x) ==  snd(x).0
Lemma: test-aprog-1_wf
∀[x:test-prog()]. test-aprog-1(x) ∈ Atom supposing ↑test-aprog?(x)
Definition: test-iterate-1
test-iterate-1(x) ==  snd(x).0
Lemma: test-iterate-1_wf
∀[x:test-prog()]. test-iterate-1(x) ∈ test-foo() supposing ↑test-iterate?(x)
Definition: test-test-1
test-test-1(x) ==  snd(x).0
Lemma: test-test-1_wf
∀[x:test-prog()]. test-test-1(x) ∈ test-prop() supposing ↑test-test?(x)
Definition: test-afoo-1
test-afoo-1(x) ==  snd(x).0
Lemma: test-afoo-1_wf
∀[x:test-foo()]. test-afoo-1(x) ∈ Atom supposing ↑test-afoo?(x)
Definition: test-bar-1
test-bar-1(x) ==  snd(x).0
Lemma: test-bar-1_wf
∀[x:test-foo()]. test-bar-1(x) ∈ test-foo() supposing ↑test-bar?(x)
Definition: test-xx-1
test-xx-1(x) ==  snd(x).0
Lemma: test-xx-1_wf
∀[x:test-foo()]. test-xx-1(x) ∈ test-prop() supposing ↑test-xx?(x)
Definition: test-xx-2
test-xx-2(x) ==  snd(x).1
Lemma: test-xx-2_wf
∀[x:test-foo()]. test-xx-2(x) ∈ test-prog() supposing ↑test-xx?(x)
Definition: test-aprop-1
test-aprop-1(x) ==  snd(x).0
Lemma: test-aprop-1_wf
∀[x:test-prop()]. test-aprop-1(x) ∈ Atom supposing ↑test-aprop?(x)
Definition: test-implies-1
test-implies-1(x) ==  snd(x).0
Lemma: test-implies-1_wf
∀[x:test-prop()]. test-implies-1(x) ∈ test-prop() supposing ↑test-implies?(x)
Definition: test-implies-2
test-implies-2(x) ==  snd(x).1
Lemma: test-implies-2_wf
∀[x:test-prop()]. test-implies-2(x) ∈ test-prop() supposing ↑test-implies?(x)
Definition: test-box-1
test-box-1(x) ==  snd(x).0
Lemma: test-box-1_wf
∀[x:test-prop()]. test-box-1(x) ∈ test-prog() supposing ↑test-box?(x)
Definition: test-box-2
test-box-2(x) ==  snd(x).1
Lemma: test-box-2_wf
∀[x:test-prop()]. test-box-2(x) ∈ test-prop() supposing ↑test-box?(x)
Definition: test-diamond-1
test-diamond-1(x) ==  snd(x).0
Lemma: test-diamond-1_wf
∀[x:test-prop()]. test-diamond-1(x) ∈ test-foo() supposing ↑test-diamond?(x)
Definition: test-diamond-2
test-diamond-2(x) ==  snd(x).1
Lemma: test-diamond-2_wf
∀[x:test-prop()]. test-diamond-2(x) ∈ test-prop() supposing ↑test-diamond?(x)
Lemma: test-induction
∀[T:test-Obj() ⟶ TYPE]
  ((∀x:Atom. T[test-prog-obj(test-aprog(x))])
  
⇒ (∀x:test-foo(). (T[test-foo-obj(x)] 
⇒ T[test-prog-obj(test-iterate(x))]))
  
⇒ (∀x:test-prop(). (T[test-prop-obj(x)] 
⇒ T[test-prog-obj(test-test(x))]))
  
⇒ (∀x:Atom. T[test-foo-obj(test-afoo(x))])
  
⇒ (∀x:test-foo(). (T[test-foo-obj(x)] 
⇒ T[test-foo-obj(test-bar(x))]))
  
⇒ (∀x:test-prop(). ∀x1:test-prog().  (T[test-prop-obj(x)] 
⇒ T[test-prog-obj(x1)] 
⇒ T[test-foo-obj(test-xx(x;x1))]))
  
⇒ (∀x:Atom. T[test-prop-obj(test-aprop(x))])
  
⇒ T[test-prop-obj(test-false())]
  
⇒ (∀x,x1:test-prop().  (T[test-prop-obj(x)] 
⇒ T[test-prop-obj(x1)] 
⇒ T[test-prop-obj(test-implies(x;x1))]))
  
⇒ (∀x:test-prog(). ∀x1:test-prop().
        (T[test-prog-obj(x)] 
⇒ T[test-prop-obj(x1)] 
⇒ T[test-prop-obj(test-box(x;x1))]))
  
⇒ (∀x:test-foo(). ∀x1:test-prop().
        (T[test-foo-obj(x)] 
⇒ T[test-prop-obj(x1)] 
⇒ T[test-prop-obj(test-diamond(x;x1))]))
  
⇒ (∀x:test-Obj(). T[x]))
Definition: test-ind
test-ind(
         test-aprog(x0)
⇒ aprog[x0];
         test-iterate(x1)
⇒ x2.iterate[x1; x2];
         test-test(x3)
⇒ x4.test[x3; x4];
         test-afoo(x5)
⇒ afoo[x5];
         test-bar(x6)
⇒ x7.bar[x6; x7];
         test-xx(x8,x9)
⇒ x10,x11.xx[x8;
                                     x9;
                                     x10;
                                     x11];
         test-aprop(x12)
⇒ aprop[x12];
         test-false
⇒ false;
         test-implies(x13,x14)
⇒ x15,x16.implies[x13;
                                                 x14;
                                                 x15;
                                                 x16];
         test-box(x17,x18)
⇒ x19,x20.box[x17;
                                         x18;
                                         x19;
                                         x20];
         test-diamond(x21,x22)
⇒ x23,x24.diamond[x21;
                                                 x22;
                                                 x23;
                                                 x24])  ==
  TERMOF{test-induction:o, 1:l} (λx0.aprog[x0]) (λx1,x2. iterate[x1; x2]) (λx3,x4. test[x3; x4]) (λx5.afoo[x5]) (λx6,x7.\000C bar[x6; x7]) 
  (λx8,x9,x10,x11. xx[x8;
                      x9;
                      x10;
                      x11]) 
  (λx12.aprop[x12]) 
  false 
  (λx13,x14,x15,x16. implies[x13;
                             x14;
                             x15;
                             x16]) 
  (λx17,x18,x19,x20. box[x17;
                         x18;
                         x19;
                         x20]) 
  (λx21,x22,x23,x24. diamond[x21;
                             x22;
                             x23;
                             x24])
Lemma: test-ind_wf
∀[T:test-Obj() ⟶ TYPE]. ∀[aprog:x:Atom ⟶ T[test-prog-obj(test-aprog(x))]].
∀[iterate:x:test-foo() ⟶ T[test-foo-obj(x)] ⟶ T[test-prog-obj(test-iterate(x))]].
∀[test:x:test-prop() ⟶ T[test-prop-obj(x)] ⟶ T[test-prog-obj(test-test(x))]].
∀[afoo:x:Atom ⟶ T[test-foo-obj(test-afoo(x))]]. ∀[bar:x:test-foo()
                                                       ⟶ T[test-foo-obj(x)]
                                                       ⟶ T[test-foo-obj(test-bar(x))]].
∀[xx:x:test-prop() ⟶ x1:test-prog() ⟶ T[test-prop-obj(x)] ⟶ T[test-prog-obj(x1)] ⟶ T[test-foo-obj(test-xx(x;x1))]].
∀[aprop:x:Atom ⟶ T[test-prop-obj(test-aprop(x))]]. ∀[false:T[test-prop-obj(test-false())]].
∀[implies:x:test-prop()
          ⟶ x1:test-prop()
          ⟶ T[test-prop-obj(x)]
          ⟶ T[test-prop-obj(x1)]
          ⟶ T[test-prop-obj(test-implies(x;x1))]]. ∀[box:x:test-prog()
                                                          ⟶ x1:test-prop()
                                                          ⟶ T[test-prog-obj(x)]
                                                          ⟶ T[test-prop-obj(x1)]
                                                          ⟶ T[test-prop-obj(test-box(x;x1))]].
∀[diamond:x:test-foo()
          ⟶ x1:test-prop()
          ⟶ T[test-foo-obj(x)]
          ⟶ T[test-prop-obj(x1)]
          ⟶ T[test-prop-obj(test-diamond(x;x1))]].
  (test-ind(
            test-aprog(x0)
⇒ aprog[x0];
            test-iterate(x1)
⇒ x2.iterate[x1;x2];
            test-test(x3)
⇒ x4.test[x3;x4];
            test-afoo(x5)
⇒ afoo[x5];
            test-bar(x6)
⇒ x7.bar[x6;x7];
            test-xx(x8,x9)
⇒ x10,x11.xx[x8;x9;x10;x11];
            test-aprop(x12)
⇒ aprop[x12];
            test-false
⇒ false;
            test-implies(x13,x14)
⇒ x15,x16.implies[x13;x14;x15;x16];
            test-box(x17,x18)
⇒ x19,x20.box[x17;x18;x19;x20];
            test-diamond(x21,x22)
⇒ x23,x24.diamond[x21;x22;x23;x24])  ∈ ∀x:test-Obj(). T[x])
Lemma: test-ind_wf_definition
∀[A,B,C:TYPE]. ∀[aprog:x:Atom ⟶ A]. ∀[iterate:x:test-foo() ⟶ B ⟶ A]. ∀[test:x:test-prop() ⟶ C ⟶ A].
∀[afoo:x:Atom ⟶ B]. ∀[bar:x:test-foo() ⟶ B ⟶ B]. ∀[xx:x:test-prop() ⟶ x1:test-prog() ⟶ C ⟶ A ⟶ B]. ∀[aprop:x:Atom
                                                                                                                  ⟶ C].
∀[false:C]. ∀[implies:x:test-prop() ⟶ x1:test-prop() ⟶ C ⟶ C ⟶ C]. ∀[box:x:test-prog()
                                                                             ⟶ x1:test-prop()
                                                                             ⟶ A
                                                                             ⟶ C
                                                                             ⟶ C]. ∀[diamond:x:test-foo()
                                                                                              ⟶ x1:test-prop()
                                                                                              ⟶ B
                                                                                              ⟶ C
                                                                                              ⟶ C].
  (test-ind(
            test-aprog(x0)
⇒ aprog[x0];
            test-iterate(x1)
⇒ x2.iterate[x1;x2];
            test-test(x3)
⇒ x4.test[x3;x4];
            test-afoo(x5)
⇒ afoo[x5];
            test-bar(x6)
⇒ x7.bar[x6;x7];
            test-xx(x8,x9)
⇒ x10,x11.xx[x8;x9;x10;x11];
            test-aprop(x12)
⇒ aprop[x12];
            test-false
⇒ false;
            test-implies(x13,x14)
⇒ x15,x16.implies[x13;x14;x15;x16];
            test-box(x17,x18)
⇒ x19,x20.box[x17;x18;x19;x20];
            test-diamond(x21,x22)
⇒ x23,x24.diamond[x21;x22;x23;x24])  ∈ d:test-Obj() ⟶ if test-kind(d) =a "prog"
                                                                                           then A
                                                                                         if test-kind(d) =a "foo" then B
                                                                                         else C
                                                                                         fi )
Lemma: test-ind-test-aprog
∀[aprog,iterate,test,afoo,bar,xx,aprop,false,implies,box,diamond,x:Top].
  (test-ind(
            test-aprog(x0)
⇒ aprog[x0];
            test-iterate(x1)
⇒ x2.iterate[x1;x2];
            test-test(x3)
⇒ x4.test[x3;x4];
            test-afoo(x5)
⇒ afoo[x5];
            test-bar(x6)
⇒ x7.bar[x6;x7];
            test-xx(x8,x9)
⇒ x10,x11.xx[x8;x9;x10;x11];
            test-aprop(x12)
⇒ aprop[x12];
            test-false
⇒ false;
            test-implies(x13,x14)
⇒ x15,x16.implies[x13;x14;x15;x16];
            test-box(x17,x18)
⇒ x19,x20.box[x17;x18;x19;x20];
            test-diamond(x21,x22)
⇒ x23,x24.diamond[x21;x22;x23;x24])  
   test-prog-obj(test-aprog(x)) ~ aprog[x])
Lemma: test-ind-test-iterate
∀[aprog,iterate,test,afoo,bar,xx,aprop,false,implies,box,diamond,x:Top].
  (test-ind(
            test-aprog(x0)
⇒ aprog[x0];
            test-iterate(x1)
⇒ x2.iterate[x1;x2];
            test-test(x3)
⇒ x4.test[x3;x4];
            test-afoo(x5)
⇒ afoo[x5];
            test-bar(x6)
⇒ x7.bar[x6;x7];
            test-xx(x8,x9)
⇒ x10,x11.xx[x8;x9;x10;x11];
            test-aprop(x12)
⇒ aprop[x12];
            test-false
⇒ false;
            test-implies(x13,x14)
⇒ x15,x16.implies[x13;x14;x15;x16];
            test-box(x17,x18)
⇒ x19,x20.box[x17;x18;x19;x20];
            test-diamond(x21,x22)
⇒ x23,x24.diamond[x21;x22;x23;x24])  
   test-prog-obj(test-iterate(x)) ~ iterate[x;test-ind(
                                                       test-aprog(x0)
⇒ aprog[x0];
                                                       test-iterate(x1)
⇒ x2.iterate[x1;x2];
                                                       test-test(x3)
⇒ x4.test[x3;x4];
                                                       test-afoo(x5)
⇒ afoo[x5];
                                                       test-bar(x6)
⇒ x7.bar[x6;x7];
                                                       test-xx(x8,x9)
⇒ x10,x11.xx[x8;x9;x10;x11];
                                                       test-aprop(x12)
⇒ aprop[x12];
                                                       test-false
⇒ false;
                                                       test-implies(x13,x14)
⇒ x15,x16.implies[x13;x14;x15;x16];
                                                       test-box(x17,x18)
⇒ x19,x20.box[x17;x18;x19;x20];
                                                       test-diamond(x21,x22)
⇒ x23,x24.diamond[x21;x22;x23;x24])  
                                              test-foo-obj(x)])
Lemma: test-ind-test-test
∀[aprog,iterate,test,afoo,bar,xx,aprop,false,implies,box,diamond,x:Top].
  (test-ind(
            test-aprog(x0)
⇒ aprog[x0];
            test-iterate(x1)
⇒ x2.iterate[x1;x2];
            test-test(x3)
⇒ x4.test[x3;x4];
            test-afoo(x5)
⇒ afoo[x5];
            test-bar(x6)
⇒ x7.bar[x6;x7];
            test-xx(x8,x9)
⇒ x10,x11.xx[x8;x9;x10;x11];
            test-aprop(x12)
⇒ aprop[x12];
            test-false
⇒ false;
            test-implies(x13,x14)
⇒ x15,x16.implies[x13;x14;x15;x16];
            test-box(x17,x18)
⇒ x19,x20.box[x17;x18;x19;x20];
            test-diamond(x21,x22)
⇒ x23,x24.diamond[x21;x22;x23;x24])  
   test-prog-obj(test-test(x)) ~ test[x;test-ind(
                                                 test-aprog(x0)
⇒ aprog[x0];
                                                 test-iterate(x1)
⇒ x2.iterate[x1;x2];
                                                 test-test(x3)
⇒ x4.test[x3;x4];
                                                 test-afoo(x5)
⇒ afoo[x5];
                                                 test-bar(x6)
⇒ x7.bar[x6;x7];
                                                 test-xx(x8,x9)
⇒ x10,x11.xx[x8;x9;x10;x11];
                                                 test-aprop(x12)
⇒ aprop[x12];
                                                 test-false
⇒ false;
                                                 test-implies(x13,x14)
⇒ x15,x16.implies[x13;x14;x15;x16];
                                                 test-box(x17,x18)
⇒ x19,x20.box[x17;x18;x19;x20];
                                                 test-diamond(x21,x22)
⇒ x23,x24.diamond[x21;x22;x23;x24])  
                                        test-prop-obj(x)])
Lemma: test-ind-test-afoo
∀[aprog,iterate,test,afoo,bar,xx,aprop,false,implies,box,diamond,x:Top].
  (test-ind(
            test-aprog(x0)
⇒ aprog[x0];
            test-iterate(x1)
⇒ x2.iterate[x1;x2];
            test-test(x3)
⇒ x4.test[x3;x4];
            test-afoo(x5)
⇒ afoo[x5];
            test-bar(x6)
⇒ x7.bar[x6;x7];
            test-xx(x8,x9)
⇒ x10,x11.xx[x8;x9;x10;x11];
            test-aprop(x12)
⇒ aprop[x12];
            test-false
⇒ false;
            test-implies(x13,x14)
⇒ x15,x16.implies[x13;x14;x15;x16];
            test-box(x17,x18)
⇒ x19,x20.box[x17;x18;x19;x20];
            test-diamond(x21,x22)
⇒ x23,x24.diamond[x21;x22;x23;x24])  
   test-foo-obj(test-afoo(x)) ~ afoo[x])
Lemma: test-ind-test-bar
∀[aprog,iterate,test,afoo,bar,xx,aprop,false,implies,box,diamond,x:Top].
  (test-ind(
            test-aprog(x0)
⇒ aprog[x0];
            test-iterate(x1)
⇒ x2.iterate[x1;x2];
            test-test(x3)
⇒ x4.test[x3;x4];
            test-afoo(x5)
⇒ afoo[x5];
            test-bar(x6)
⇒ x7.bar[x6;x7];
            test-xx(x8,x9)
⇒ x10,x11.xx[x8;x9;x10;x11];
            test-aprop(x12)
⇒ aprop[x12];
            test-false
⇒ false;
            test-implies(x13,x14)
⇒ x15,x16.implies[x13;x14;x15;x16];
            test-box(x17,x18)
⇒ x19,x20.box[x17;x18;x19;x20];
            test-diamond(x21,x22)
⇒ x23,x24.diamond[x21;x22;x23;x24])  
   test-foo-obj(test-bar(x)) ~ bar[x;test-ind(
                                              test-aprog(x0)
⇒ aprog[x0];
                                              test-iterate(x1)
⇒ x2.iterate[x1;x2];
                                              test-test(x3)
⇒ x4.test[x3;x4];
                                              test-afoo(x5)
⇒ afoo[x5];
                                              test-bar(x6)
⇒ x7.bar[x6;x7];
                                              test-xx(x8,x9)
⇒ x10,x11.xx[x8;x9;x10;x11];
                                              test-aprop(x12)
⇒ aprop[x12];
                                              test-false
⇒ false;
                                              test-implies(x13,x14)
⇒ x15,x16.implies[x13;x14;x15;x16];
                                              test-box(x17,x18)
⇒ x19,x20.box[x17;x18;x19;x20];
                                              test-diamond(x21,x22)
⇒ x23,x24.diamond[x21;x22;x23;x24])  
                                     test-foo-obj(x)])
Lemma: test-ind-test-xx
∀[aprog,iterate,test,afoo,bar,xx,aprop,false,implies,box,diamond,x,x1:Top].
  (test-ind(
            test-aprog(x0)
⇒ aprog[x0];
            test-iterate(x1)
⇒ x2.iterate[x1;x2];
            test-test(x3)
⇒ x4.test[x3;x4];
            test-afoo(x5)
⇒ afoo[x5];
            test-bar(x6)
⇒ x7.bar[x6;x7];
            test-xx(x8,x9)
⇒ x10,x11.xx[x8;x9;x10;x11];
            test-aprop(x12)
⇒ aprop[x12];
            test-false
⇒ false;
            test-implies(x13,x14)
⇒ x15,x16.implies[x13;x14;x15;x16];
            test-box(x17,x18)
⇒ x19,x20.box[x17;x18;x19;x20];
            test-diamond(x21,x22)
⇒ x23,x24.diamond[x21;x22;x23;x24])  
   test-foo-obj(test-xx(x;x1)) ~ xx[x;x1;test-ind(
                                                  test-aprog(x0)
⇒ aprog[x0];
                                                  test-iterate(x1)
⇒ x2.iterate[x1;x2];
                                                  test-test(x3)
⇒ x4.test[x3;x4];
                                                  test-afoo(x5)
⇒ afoo[x5];
                                                  test-bar(x6)
⇒ x7.bar[x6;x7];
                                                  test-xx(x8,x9)
⇒ x10,x11.xx[x8;x9;x10;x11];
                                                  test-aprop(x12)
⇒ aprop[x12];
                                                  test-false
⇒ false;
                                                  test-implies(x13,x14)
⇒ x15,x16.implies[x13;x14;x15;x16];
                                                  test-box(x17,x18)
⇒ x19,x20.box[x17;x18;x19;x20];
                                                  test-diamond(x21,x22)
⇒ x23,x24.diamond[x21;x22;x23;x24])  
                                         test-prop-obj(x);test-ind(
                                                                   test-aprog(x0)
⇒ aprog[x0];
                                                                   test-iterate(x1)
⇒ x2.iterate[x1;x2];
                                                                   test-test(x3)
⇒ x4.test[x3;x4];
                                                                   test-afoo(x5)
⇒ afoo[x5];
                                                                   test-bar(x6)
⇒ x7.bar[x6;x7];
                                                                   test-xx(x8,x9)
⇒ x10,x11.xx[x8;x9;x10;x11];
                                                                   test-aprop(x12)
⇒ aprop[x12];
                                                                   test-false
⇒ false;
                                                                   test-implies(x13,x14)
⇒ x15,x16.implies[x13;x14;x15;
                                                                                                          x16];
                                                                   test-box(x17,x18)
⇒ x19,x20.box[x17;x18;x19;x20];
                                                                   test-diamond(x21,x22)
⇒ x23,x24.diamond[x21;x22;x23;
                                                                                                          x24])  
                                                          test-prog-obj(x1)])
Lemma: test-ind-test-aprop
∀[aprog,iterate,test,afoo,bar,xx,aprop,false,implies,box,diamond,x:Top].
  (test-ind(
            test-aprog(x0)
⇒ aprog[x0];
            test-iterate(x1)
⇒ x2.iterate[x1;x2];
            test-test(x3)
⇒ x4.test[x3;x4];
            test-afoo(x5)
⇒ afoo[x5];
            test-bar(x6)
⇒ x7.bar[x6;x7];
            test-xx(x8,x9)
⇒ x10,x11.xx[x8;x9;x10;x11];
            test-aprop(x12)
⇒ aprop[x12];
            test-false
⇒ false;
            test-implies(x13,x14)
⇒ x15,x16.implies[x13;x14;x15;x16];
            test-box(x17,x18)
⇒ x19,x20.box[x17;x18;x19;x20];
            test-diamond(x21,x22)
⇒ x23,x24.diamond[x21;x22;x23;x24])  
   test-prop-obj(test-aprop(x)) ~ aprop[x])
Lemma: test-ind-test-false
∀[aprog,iterate,test,afoo,bar,xx,aprop,false,implies,box,diamond:Top].
  (test-ind(
            test-aprog(x0)
⇒ aprog[x0];
            test-iterate(x1)
⇒ x2.iterate[x1;x2];
            test-test(x3)
⇒ x4.test[x3;x4];
            test-afoo(x5)
⇒ afoo[x5];
            test-bar(x6)
⇒ x7.bar[x6;x7];
            test-xx(x8,x9)
⇒ x10,x11.xx[x8;x9;x10;x11];
            test-aprop(x12)
⇒ aprop[x12];
            test-false
⇒ false;
            test-implies(x13,x14)
⇒ x15,x16.implies[x13;x14;x15;x16];
            test-box(x17,x18)
⇒ x19,x20.box[x17;x18;x19;x20];
            test-diamond(x21,x22)
⇒ x23,x24.diamond[x21;x22;x23;x24])  
   test-prop-obj(test-false()) ~ false)
Lemma: test-ind-test-implies
∀[aprog,iterate,test,afoo,bar,xx,aprop,false,implies,box,diamond,x,x1:Top].
  (test-ind(
            test-aprog(x0)
⇒ aprog[x0];
            test-iterate(x1)
⇒ x2.iterate[x1;x2];
            test-test(x3)
⇒ x4.test[x3;x4];
            test-afoo(x5)
⇒ afoo[x5];
            test-bar(x6)
⇒ x7.bar[x6;x7];
            test-xx(x8,x9)
⇒ x10,x11.xx[x8;x9;x10;x11];
            test-aprop(x12)
⇒ aprop[x12];
            test-false
⇒ false;
            test-implies(x13,x14)
⇒ x15,x16.implies[x13;x14;x15;x16];
            test-box(x17,x18)
⇒ x19,x20.box[x17;x18;x19;x20];
            test-diamond(x21,x22)
⇒ x23,x24.diamond[x21;x22;x23;x24])  
   test-prop-obj(test-implies(x;x1)) 
  ~ implies[x;x1;test-ind(
                          test-aprog(x0)
⇒ aprog[x0];
                          test-iterate(x1)
⇒ x2.iterate[x1;x2];
                          test-test(x3)
⇒ x4.test[x3;x4];
                          test-afoo(x5)
⇒ afoo[x5];
                          test-bar(x6)
⇒ x7.bar[x6;x7];
                          test-xx(x8,x9)
⇒ x10,x11.xx[x8;x9;x10;x11];
                          test-aprop(x12)
⇒ aprop[x12];
                          test-false
⇒ false;
                          test-implies(x13,x14)
⇒ x15,x16.implies[x13;x14;x15;x16];
                          test-box(x17,x18)
⇒ x19,x20.box[x17;x18;x19;x20];
                          test-diamond(x21,x22)
⇒ x23,x24.diamond[x21;x22;x23;x24])  
                 test-prop-obj(x);test-ind(
                                           test-aprog(x0)
⇒ aprog[x0];
                                           test-iterate(x1)
⇒ x2.iterate[x1;x2];
                                           test-test(x3)
⇒ x4.test[x3;x4];
                                           test-afoo(x5)
⇒ afoo[x5];
                                           test-bar(x6)
⇒ x7.bar[x6;x7];
                                           test-xx(x8,x9)
⇒ x10,x11.xx[x8;x9;x10;x11];
                                           test-aprop(x12)
⇒ aprop[x12];
                                           test-false
⇒ false;
                                           test-implies(x13,x14)
⇒ x15,x16.implies[x13;x14;x15;x16];
                                           test-box(x17,x18)
⇒ x19,x20.box[x17;x18;x19;x20];
                                           test-diamond(x21,x22)
⇒ x23,x24.diamond[x21;x22;x23;x24])  
                                  test-prop-obj(x1)])
Lemma: test-ind-test-box
∀[aprog,iterate,test,afoo,bar,xx,aprop,false,implies,box,diamond,x,x1:Top].
  (test-ind(
            test-aprog(x0)
⇒ aprog[x0];
            test-iterate(x1)
⇒ x2.iterate[x1;x2];
            test-test(x3)
⇒ x4.test[x3;x4];
            test-afoo(x5)
⇒ afoo[x5];
            test-bar(x6)
⇒ x7.bar[x6;x7];
            test-xx(x8,x9)
⇒ x10,x11.xx[x8;x9;x10;x11];
            test-aprop(x12)
⇒ aprop[x12];
            test-false
⇒ false;
            test-implies(x13,x14)
⇒ x15,x16.implies[x13;x14;x15;x16];
            test-box(x17,x18)
⇒ x19,x20.box[x17;x18;x19;x20];
            test-diamond(x21,x22)
⇒ x23,x24.diamond[x21;x22;x23;x24])  
   test-prop-obj(test-box(x;x1)) ~ box[x;x1;test-ind(
                                                     test-aprog(x0)
⇒ aprog[x0];
                                                     test-iterate(x1)
⇒ x2.iterate[x1;x2];
                                                     test-test(x3)
⇒ x4.test[x3;x4];
                                                     test-afoo(x5)
⇒ afoo[x5];
                                                     test-bar(x6)
⇒ x7.bar[x6;x7];
                                                     test-xx(x8,x9)
⇒ x10,x11.xx[x8;x9;x10;x11];
                                                     test-aprop(x12)
⇒ aprop[x12];
                                                     test-false
⇒ false;
                                                     test-implies(x13,x14)
⇒ x15,x16.implies[x13;x14;x15;x16];
                                                     test-box(x17,x18)
⇒ x19,x20.box[x17;x18;x19;x20];
                                                     test-diamond(x21,x22)
⇒ x23,x24.diamond[x21;x22;x23;x24])  
                                            test-prog-obj(x);test-ind(
                                                                      test-aprog(x0)
⇒ aprog[x0];
                                                                      test-iterate(x1)
⇒ x2.iterate[x1;x2];
                                                                      test-test(x3)
⇒ x4.test[x3;x4];
                                                                      test-afoo(x5)
⇒ afoo[x5];
                                                                      test-bar(x6)
⇒ x7.bar[x6;x7];
                                                                      test-xx(x8,x9)
⇒ x10,x11.xx[x8;x9;x10;x11];
                                                                      test-aprop(x12)
⇒ aprop[x12];
                                                                      test-false
⇒ false;
                                                                      test-implies(x13,x14)
⇒ x15,x16.implies[x13;x14;
                                                                                                             x15;x16];
                                                                      test-box(x17,x18)
⇒ x19,x20.box[x17;x18;x19;x20];
                                                                      test-diamond(x21,x22)
⇒ x23,x24.diamond[x21;x22;
                                                                                                             x23;x24])  
                                                             test-prop-obj(x1)])
Lemma: test-ind-test-diamond
∀[aprog,iterate,test,afoo,bar,xx,aprop,false,implies,box,diamond,x,x1:Top].
  (test-ind(
            test-aprog(x0)
⇒ aprog[x0];
            test-iterate(x1)
⇒ x2.iterate[x1;x2];
            test-test(x3)
⇒ x4.test[x3;x4];
            test-afoo(x5)
⇒ afoo[x5];
            test-bar(x6)
⇒ x7.bar[x6;x7];
            test-xx(x8,x9)
⇒ x10,x11.xx[x8;x9;x10;x11];
            test-aprop(x12)
⇒ aprop[x12];
            test-false
⇒ false;
            test-implies(x13,x14)
⇒ x15,x16.implies[x13;x14;x15;x16];
            test-box(x17,x18)
⇒ x19,x20.box[x17;x18;x19;x20];
            test-diamond(x21,x22)
⇒ x23,x24.diamond[x21;x22;x23;x24])  
   test-prop-obj(test-diamond(x;x1)) 
  ~ diamond[x;x1;test-ind(
                          test-aprog(x0)
⇒ aprog[x0];
                          test-iterate(x1)
⇒ x2.iterate[x1;x2];
                          test-test(x3)
⇒ x4.test[x3;x4];
                          test-afoo(x5)
⇒ afoo[x5];
                          test-bar(x6)
⇒ x7.bar[x6;x7];
                          test-xx(x8,x9)
⇒ x10,x11.xx[x8;x9;x10;x11];
                          test-aprop(x12)
⇒ aprop[x12];
                          test-false
⇒ false;
                          test-implies(x13,x14)
⇒ x15,x16.implies[x13;x14;x15;x16];
                          test-box(x17,x18)
⇒ x19,x20.box[x17;x18;x19;x20];
                          test-diamond(x21,x22)
⇒ x23,x24.diamond[x21;x22;x23;x24])  
                 test-foo-obj(x);test-ind(
                                          test-aprog(x0)
⇒ aprog[x0];
                                          test-iterate(x1)
⇒ x2.iterate[x1;x2];
                                          test-test(x3)
⇒ x4.test[x3;x4];
                                          test-afoo(x5)
⇒ afoo[x5];
                                          test-bar(x6)
⇒ x7.bar[x6;x7];
                                          test-xx(x8,x9)
⇒ x10,x11.xx[x8;x9;x10;x11];
                                          test-aprop(x12)
⇒ aprop[x12];
                                          test-false
⇒ false;
                                          test-implies(x13,x14)
⇒ x15,x16.implies[x13;x14;x15;x16];
                                          test-box(x17,x18)
⇒ x19,x20.box[x17;x18;x19;x20];
                                          test-diamond(x21,x22)
⇒ x23,x24.diamond[x21;x22;x23;x24])  
                                 test-prop-obj(x1)])
Lemma: test-mrec-reduce
test-ind(
         test-aprog(x)
⇒ 1;
         test-iterate(x)
⇒ x.2;
         test-test(x)
⇒ x.3;
         test-afoo(x)
⇒ 4;
         test-bar(x)
⇒ x.5;
         test-xx(x,x)
⇒ x,x.6;
         test-aprop(x)
⇒ 7;
         test-false
⇒ 99;
         test-implies(a,b)
⇒ x,c.c;
         test-box(x,x)
⇒ x,x.9;
         test-diamond(x,x)
⇒ x,x.10)  
test-prop-obj(test-implies(22;33)) ~ test-ind(
                                              test-aprog(x)
⇒ 1;
                                              test-iterate(x)
⇒ x.2;
                                              test-test(x)
⇒ x.3;
                                              test-afoo(x)
⇒ 4;
                                              test-bar(x)
⇒ x.5;
                                              test-xx(x,x)
⇒ x,x.6;
                                              test-aprop(x)
⇒ 7;
                                              test-false
⇒ 99;
                                              test-implies(a,b)
⇒ x,c.c;
                                              test-box(x,x)
⇒ x,x.9;
                                              test-diamond(x,x)
⇒ x,x.10)  
                                     test-prop-obj(33)
Home
Index