[mizar] a question about a proof and a method

["Ozyavas, Adem" <adem.ozyavas@ttu.edu>]

Dear All,

I am struggling with a method of how to get around typing requirements which I try to explain and a proof.
Hopefully, my questions will make it a bit clear what I mean by this typing issue. Before I asking my questions I am giving a partial definition 
of a functor called 'sexp' where the type of its second argument matters and a proof of another functor called 'distr'. 
My questions follow the Mizar text given below. 


definition
  let op be real number;
  let arg be FinSequence;
  func sexp(op,arg) -> FinSequence means
    ...
end;




definition
  let o be real number, fs be FinSequence;
  assume TAS: 1 <= len fs;
  func distr(o,fs) -> FinSequence means
    dom it = Seg(len fs) &
    it.1 = S &
    for i being Nat st i in Seg(len fs)\{1} holds
      ex p being FinSequence st p = fs.i & it.i = sexp(o,p);
   existence
   proof
     defpred P[set,set] means ex n being Nat st n = $1 &
     (n = 1 implies $2 = S) &
     (2<= n & n <= len fs implies ex p being FinSequence st p = fs.n & ::variable p!!
      $2 = sexp(o,p));

     for x being set st x in Seg(len fs) holds ex y being set st P[x,y]
     proof
       let x be set;
       assume AS: x in Seg(len fs);
       then reconsider x' = x as Element of NAT;
       Seg(len fs) = Seg(len fs)\{1} \/ {1}
       proof
        Seg 1 c= Seg(len fs) by TAS,FINSEQ_1:7;
        then {1} c= Seg(len fs) by FINSEQ_1:4;
        hence thesis by Seg1;
       end;
       then PC: x in Seg(len fs)\{1} or x in {1} by AS, XBOOLE_0:def 2;
       per cases by PC;
       suppose Sn1: x in Seg(len fs)\{1};
         x in Seg(len fs) & not x in {1} by Sn1,XBOOLE_0:def 4;
         then NE1: x <> 1 by TARSKI:def 1;
         
         ??????????   ::trying to prove this part

       end;
       suppose Se1: x in {1};
         EQ: x = 1 by Se1,TARSKI:def 1;
         take S;
         take x';
         thus x' = x;
         thus (x' = 1 implies S = S);
         thus thesis by EQ;
       end;
     end;
   end;
::>  *70
   uniqueness
   proof
   end;
::>  *70
end;


Q1) I used the existentially quantified variable *p* of type FinSequence  both in the 
'distr' functor and inside the predicate P definition to get around the typing requirement
 of 'sexp' functor which expects its second argument to be of type FinSequence. 
Is this an acceptable method to satisfy typing requirement as in my example?

Q2) Can the following 
     
    for p being FinSequence st p = fs.n holds $2 = sexp(o,p));

    be used interchangeably with the existentially quantified version given both in the 'distr' and 
    predicate P definition for the same purpose, that is, to satisfy the typing requirement
    of sexp? 

Q3) How do I prove the missing part which I marked with ????????  ?
I have tried it all day today and could not find a way to prove it. 


Note: S is a constant I defined which is not included here (it.1 = S in the above text). S is defined to be
a real number. Seg1 is another statement I proved in my file and it is given below:

Seg1:
for A,B being set st A c= B holds (B\A)\/ A = B
proof
  let A,B be set;
  assume AS: A c= B;
  (B\A) \/ A = B \/ A by XBOOLE_1:39
                 .= B by AS,XBOOLE_1:12;
  hence thesis;
end;


Thank you for all your help and I cannot express enough my thanks for all the help I have been getting so far...

Adem Ozyavas
Texas Tech University
Computer Science Department