amistd_3.miz



    begin

    reserve x,y,z,X for set,

m,n for Nat,

O for Ordinal,

R,S for Relation;

    reserve N for with_zero set,

S for standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N,

L,l1 for Nat,

J for Instruction of S,

F for Subset of NAT ;

    definition

      let N be with_zero set, S be standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, M be Subset of NAT ;

      deffunc F( object) = (( canonical_isomorphism_of (( RelIncl ( order_type_of ( RelIncl M))),( RelIncl M))) . $1);

      :: AMISTD_3:def1

      func LocSeq (M,S) -> Sequence of NAT means

      : Def1: ( dom it ) = ( card M) & for m be set st m in ( card M) holds (it . m) = (( canonical_isomorphism_of (( RelIncl ( order_type_of ( RelIncl M))),( RelIncl M))) . m);

      existence

      proof

        consider f be Sequence such that

         A1: ( dom f) = ( card M) and

         A2: for A be Ordinal st A in ( card M) holds (f . A) = F(A) from ORDINAL2:sch 2;

        f is NAT -valued

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A3: x in ( dom f) & y = (f . x) by FUNCT_1:def 3;

          reconsider x as set by TARSKI: 1;

           F(x) in NAT by ORDINAL1:def 12;

          hence thesis by A1, A2, A3;

        end;

        then

        reconsider f as Sequence of NAT ;

        take f;

        thus ( dom f) = ( card M) by A1;

        let m be set;

        assume m in ( card M);

        hence thesis by A2;

      end;

      uniqueness

      proof

        let f,g be Sequence of NAT such that

         A4: ( dom f) = ( card M) and

         A5: for m be set st m in ( card M) holds (f . m) = F(m) and

         A6: ( dom g) = ( card M) and

         A7: for m be set st m in ( card M) holds (g . m) = F(m);

        for x be object st x in ( dom f) holds (f . x) = (g . x)

        proof

          let x be object such that

           A8: x in ( dom f);

          

          thus (f . x) = F(x) by A4, A5, A8

          .= (g . x) by A4, A7, A8;

        end;

        hence thesis by A4, A6;

      end;

    end

    theorem :: AMISTD_3:1

    F = {n} implies ( LocSeq (F,S)) = ( 0 .--> n)

    proof

      assume

       A1: F = {n};

      then

       A2: ( card F) = { 0 } by CARD_1: 30, CARD_1: 49;

       {n} c= omega by ORDINAL1:def 12;

      

      then

       A3: (( canonical_isomorphism_of (( RelIncl ( order_type_of ( RelIncl {n}))),( RelIncl {n}))) . 0 ) = (( 0 .--> n) . 0 ) by CARD_5: 38

      .= n by FUNCOP_1: 72;

      

       A4: ( dom ( LocSeq (F,S))) = ( card F) by Def1;

      

       A5: for a be object st a in ( dom ( LocSeq (F,S))) holds (( LocSeq (F,S)) . a) = (( 0 .--> n) . a)

      proof

        let a be object;

        assume

         A6: a in ( dom ( LocSeq (F,S)));

        then

         A7: a = 0 by A4, A2, TARSKI:def 1;

        

        thus (( LocSeq (F,S)) . a) = (( canonical_isomorphism_of (( RelIncl ( order_type_of ( RelIncl F))),( RelIncl F))) . a) by A4, A6, Def1

        .= (( 0 .--> n) . a) by A1, A3, A7, FUNCOP_1: 72;

      end;

      thus thesis by A1, A4, A5, CARD_1: 30, CARD_1: 49;

    end;

    registration

      let N be with_zero set, S be standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, M be Subset of NAT ;

      cluster ( LocSeq (M,S)) -> one-to-one;

      coherence

      proof

        set f = ( LocSeq (M,S));

        set C = ( canonical_isomorphism_of (( RelIncl ( order_type_of ( RelIncl M))),( RelIncl M)));

        let x1,x2 be object such that

         A1: x1 in ( dom f) & x2 in ( dom f) and

         A2: (f . x1) = (f . x2);

        

         A3: ( dom f) = ( card M) by Def1;

        then

         A4: (f . x1) = (C . x1) & (f . x2) = (C . x2) by A1, Def1;

        

         A5: ( card M) c= ( order_type_of ( RelIncl M)) by CARD_5: 39;

        consider phi be Ordinal-Sequence such that

         A6: phi = C and

         A7: phi is increasing and

         A8: ( dom phi) = ( order_type_of ( RelIncl M)) and ( rng phi) = M by CARD_5: 5;

        phi is one-to-one by A7, CARD_5: 11;

        hence thesis by A1, A2, A3, A4, A6, A8, A5;

      end;

    end

    definition

      let N be with_zero set, S be standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, M be non empty preProgram of S;

      :: AMISTD_3:def2

      func ExecTree (M) -> DecoratedTree of NAT means

      : Def2: (it . {} ) = ( FirstLoc M) & for t be Element of ( dom it ) holds ( succ t) = { (t ^ <*k*>) where k be Nat : k in ( card ( NIC ((M /. (it . t)),(it . t)))) } & for m be Nat st m in ( card ( NIC ((M /. (it . t)),(it . t)))) holds (it . (t ^ <*m*>)) = (( LocSeq (( NIC ((M /. (it . t)),(it . t))),S)) . m);

      existence

      proof

        defpred S[ Nat, Nat] means $1 in ( card ( NIC ((M /. $2),$2)));

        reconsider n = ( FirstLoc M) as Nat;

        defpred P[ set, Nat, set] means ex l be Nat st l = $1 & ($2 in ( dom ( LocSeq (( NIC ((M /. l),l)),S))) implies $3 = (( LocSeq (( NIC ((M /. l),l)),S)) . $2)) & ( not $2 in ( dom ( LocSeq (( NIC ((M /. l),l)),S))) implies $3 = 0 );

        set D = NAT ;

        

         A1: for x,y be Element of NAT holds ex z be Element of NAT st P[x, y, z]

        proof

          let x,y be Element of NAT ;

          reconsider z = (( LocSeq (( NIC ((M /. x),x)),S)) . y) as Element of NAT by ORDINAL1:def 12;

          per cases ;

            suppose

             A2: y in ( dom ( LocSeq (( NIC ((M /. x),x)),S)));

            take z;

            thus thesis by A2;

          end;

            suppose

             A3: not y in ( dom ( LocSeq (( NIC ((M /. x),x)),S)));

            reconsider il = 0 as Element of NAT ;

            take il;

            thus thesis by A3;

          end;

        end;

        consider f be Function of [:D, NAT :], D such that

         A4: for l,n be Element of NAT holds P[l, n, (f . (l,n))] from BINOP_1:sch 3( A1);

        

         A5: for d be Element of NAT , k1,k2 be Nat st k1 <= k2 & S[k2, d] holds S[k1, d]

        proof

          let d be Element of NAT , k1,k2 be Nat such that

           A6: k1 <= k2 and

           A7: S[k2, d];

          ( Segm k2) in ( card ( NIC ((M /. d),d))) by A7;

          then ( Segm k1) in ( card ( NIC ((M /. d),d))) by A6, NAT_1: 39, ORDINAL1: 12;

          hence thesis;

        end;

        reconsider n as Element of NAT ;

        consider T be DecoratedTree of NAT such that

         A8: (T . {} ) = n and

         A9: for t be Element of ( dom T) holds ( succ t) = { (t ^ <*k*>) where k be Nat : S[k, (T . t)] } & for n be Nat st S[n, (T . t)] holds (T . (t ^ <*n*>)) = (f . ((T . t),n)) from TREES_2:sch 10( A5);

        take T;

        thus (T . {} ) = ( FirstLoc M) by A8;

        let t be Element of ( dom T);

        thus ( succ t) = { (t ^ <*k*>) where k be Nat : S[k, (T . t)] } by A9;

        reconsider n = (T . t) as Element of NAT ;

        let m be Nat;

        

         A10: m in NAT by ORDINAL1:def 12;

        consider l be Nat such that

         A11: l = n and

         A12: m in ( dom ( LocSeq (( NIC ((M /. l),l)),S))) implies (f . (n,m)) = (( LocSeq (( NIC ((M /. l),l)),S)) . m) and not m in ( dom ( LocSeq (( NIC ((M /. l),l)),S))) implies (f . (n,m)) = 0 by A4, A10;

        assume m in ( card ( NIC ((M /. (T . t)),(T . t))));

        hence thesis by A9, A11, A12, Def1;

      end;

      uniqueness

      proof

        let T1,T2 be DecoratedTree of NAT such that

         A13: (T1 . {} ) = ( FirstLoc M) and

         A14: for t be Element of ( dom T1) holds ( succ t) = { (t ^ <*k*>) where k be Nat : k in ( card ( NIC ((M /. (T1 . t)),(T1 . t)))) } & for m be Nat st m in ( card ( NIC ((M /. (T1 . t)),(T1 . t)))) holds (T1 . (t ^ <*m*>)) = (( LocSeq (( NIC ((M /. (T1 . t)),(T1 . t))),S)) . m) and

         A15: (T2 . {} ) = ( FirstLoc M) and

         A16: for t be Element of ( dom T2) holds ( succ t) = { (t ^ <*k*>) where k be Nat : k in ( card ( NIC ((M /. (T2 . t)),(T2 . t)))) } & for m be Nat st m in ( card ( NIC ((M /. (T2 . t)),(T2 . t)))) holds (T2 . (t ^ <*m*>)) = (( LocSeq (( NIC ((M /. (T2 . t)),(T2 . t))),S)) . m);

        defpred P[ Nat] means (( dom T1) -level $1) = (( dom T2) -level $1);

        

         A17: for n be Nat st P[n] holds P[(n + 1)]

        proof

          let n be Nat such that

           A18: P[n];

          set U2 = { ( succ w) where w be Element of ( dom T2) : ( len w) = n };

          set U1 = { ( succ w) where w be Element of ( dom T1) : ( len w) = n };

          

           A19: (( dom T2) -level n) = { v where v be Element of ( dom T2) : ( len v) = n } by TREES_2:def 6;

          

           A20: (( dom T1) -level n) = { v where v be Element of ( dom T1) : ( len v) = n } by TREES_2:def 6;

          

           A21: ( union U1) = ( union U2)

          proof

            hereby

              let a be object;

              assume a in ( union U1);

              then

              consider A be set such that

               A22: a in A and

               A23: A in U1 by TARSKI:def 4;

              consider w be Element of ( dom T1) such that

               A24: A = ( succ w) and

               A25: ( len w) = n by A23;

              w in (( dom T1) -level n) by A20, A25;

              then

              consider v be Element of ( dom T2) such that

               A26: w = v and

               A27: ( len v) = n by A18, A19;

              

               A28: w = (w | ( Seg ( len w))) by FINSEQ_3: 49;

              defpred R[ Nat] means $1 <= ( len w) & (w | ( Seg $1)) in ( dom T1) & (v | ( Seg $1)) in ( dom T2) implies (T1 . (w | ( Seg $1))) = (T2 . (w | ( Seg $1)));

              

               A29: for n be Nat st R[n] holds R[(n + 1)]

              proof

                let n be Nat;

                assume that

                 A30: R[n] and

                 A31: (n + 1) <= ( len w) and

                 A32: (w | ( Seg (n + 1))) in ( dom T1) and

                 A33: (v | ( Seg (n + 1))) in ( dom T2);

                set t1 = (w | ( Seg n));

                

                 A34: 1 <= (n + 1) by NAT_1: 11;

                

                 A35: ( len (w | ( Seg (n + 1)))) = (n + 1) by A31, FINSEQ_1: 17;

                then ( len (w | ( Seg (n + 1)))) in ( Seg (n + 1)) by A34, FINSEQ_1: 1;

                then

                 A36: (w . (n + 1)) = ((w | ( Seg (n + 1))) . ( len (w | ( Seg (n + 1))))) by A35, FUNCT_1: 49;

                (n + 1) in ( dom w) by A31, A34, FINSEQ_3: 25;

                then

                 A37: (w | ( Seg (n + 1))) = (t1 ^ <*((w | ( Seg (n + 1))) . ( len (w | ( Seg (n + 1)))))*>) by A36, FINSEQ_5: 10;

                

                 A38: n <= (n + 1) by NAT_1: 11;

                then

                 A39: ( Seg n) c= ( Seg (n + 1)) by FINSEQ_1: 5;

                then (v | ( Seg n)) = ((v | ( Seg (n + 1))) | ( Seg n)) by RELAT_1: 74;

                then

                 A40: (v | ( Seg n)) is_a_prefix_of (v | ( Seg (n + 1))) by TREES_1:def 1;

                (w | ( Seg n)) = ((w | ( Seg (n + 1))) | ( Seg n)) by A39, RELAT_1: 74;

                then (w | ( Seg n)) is_a_prefix_of (w | ( Seg (n + 1))) by TREES_1:def 1;

                then

                reconsider t1 as Element of ( dom T1) by A32, TREES_1: 20;

                reconsider t2 = t1 as Element of ( dom T2) by A26, A33, A40, TREES_1: 20;

                

                 A41: ( succ t1) = { (t1 ^ <*k*>) where k be Nat : k in ( card ( NIC ((M /. (T1 . t1)),(T1 . t1)))) } by A14;

                (t1 ^ <*((w | ( Seg (n + 1))) . ( len (w | ( Seg (n + 1)))))*>) in ( succ t1) by A32, A37, TREES_2: 12;

                then

                consider k be Nat such that

                 A42: (t1 ^ <*((w | ( Seg (n + 1))) . ( len (w | ( Seg (n + 1)))))*>) = (t1 ^ <*k*>) and

                 A43: k in ( card ( NIC ((M /. (T1 . t1)),(T1 . t1)))) by A41;

                

                 A44: ((w | ( Seg (n + 1))) . ( len (w | ( Seg (n + 1))))) in ( card ( NIC ((M /. (T2 . t2)),(T2 . t2)))) by A30, A31, A33, A38, A40, A42, A43, FINSEQ_2: 17, TREES_1: 20, XXREAL_0: 2;

                k = ((w | ( Seg (n + 1))) . ( len (w | ( Seg (n + 1))))) by A42, FINSEQ_2: 17;

                

                hence (T1 . (w | ( Seg (n + 1)))) = (( LocSeq (( NIC ((M /. (T1 . t1)),(T1 . t1))),S)) . ((w | ( Seg (n + 1))) . ( len (w | ( Seg (n + 1)))))) by A14, A37, A43

                .= (T2 . (w | ( Seg (n + 1)))) by A16, A30, A31, A33, A38, A40, A37, A44, TREES_1: 20, XXREAL_0: 2;

              end;

              

               A45: R[ 0 ] by A13, A15;

              for n be Nat holds R[n] from NAT_1:sch 2( A45, A29);

              then

               A46: (T1 . w) = (T2 . w) by A26, A28;

              

               A47: ( succ v) in U2 by A27;

              ( succ v) = { (v ^ <*k*>) where k be Nat : k in ( card ( NIC ((M /. (T2 . v)),(T2 . v)))) } & ( succ w) = { (w ^ <*k*>) where k be Nat : k in ( card ( NIC ((M /. (T1 . w)),(T1 . w)))) } by A14, A16;

              hence a in ( union U2) by A22, A24, A26, A46, A47, TARSKI:def 4;

            end;

            let a be object;

            assume a in ( union U2);

            then

            consider A be set such that

             A48: a in A and

             A49: A in U2 by TARSKI:def 4;

            consider w be Element of ( dom T2) such that

             A50: A = ( succ w) and

             A51: ( len w) = n by A49;

            w in (( dom T2) -level n) by A19, A51;

            then

            consider v be Element of ( dom T1) such that

             A52: w = v and

             A53: ( len v) = n by A18, A20;

            

             A54: w = (w | ( Seg ( len w))) by FINSEQ_3: 49;

            defpred R[ Nat] means $1 <= ( len w) & (w | ( Seg $1)) in ( dom T1) & (v | ( Seg $1)) in ( dom T2) implies (T1 . (w | ( Seg $1))) = (T2 . (w | ( Seg $1)));

            

             A55: for n be Nat st R[n] holds R[(n + 1)]

            proof

              let n be Nat;

              assume that

               A56: R[n] and

               A57: (n + 1) <= ( len w) and

               A58: (w | ( Seg (n + 1))) in ( dom T1) and

               A59: (v | ( Seg (n + 1))) in ( dom T2);

              set t1 = (w | ( Seg n));

              

               A60: 1 <= (n + 1) by NAT_1: 11;

              

               A61: ( len (w | ( Seg (n + 1)))) = (n + 1) by A57, FINSEQ_1: 17;

              then ( len (w | ( Seg (n + 1)))) in ( Seg (n + 1)) by A60, FINSEQ_1: 1;

              then

               A62: (w . (n + 1)) = ((w | ( Seg (n + 1))) . ( len (w | ( Seg (n + 1))))) by A61, FUNCT_1: 49;

              (n + 1) in ( dom w) by A57, A60, FINSEQ_3: 25;

              then

               A63: (w | ( Seg (n + 1))) = (t1 ^ <*((w | ( Seg (n + 1))) . ( len (w | ( Seg (n + 1)))))*>) by A62, FINSEQ_5: 10;

              

               A64: n <= (n + 1) by NAT_1: 11;

              then

               A65: ( Seg n) c= ( Seg (n + 1)) by FINSEQ_1: 5;

              then (v | ( Seg n)) = ((v | ( Seg (n + 1))) | ( Seg n)) by RELAT_1: 74;

              then

               A66: (v | ( Seg n)) is_a_prefix_of (v | ( Seg (n + 1))) by TREES_1:def 1;

              (w | ( Seg n)) = ((w | ( Seg (n + 1))) | ( Seg n)) by A65, RELAT_1: 74;

              then (w | ( Seg n)) is_a_prefix_of (w | ( Seg (n + 1))) by TREES_1:def 1;

              then

              reconsider t1 as Element of ( dom T1) by A58, TREES_1: 20;

              reconsider t2 = t1 as Element of ( dom T2) by A52, A59, A66, TREES_1: 20;

              

               A67: ( succ t1) = { (t1 ^ <*k*>) where k be Nat : k in ( card ( NIC ((M /. (T1 . t1)),(T1 . t1)))) } by A14;

              (t1 ^ <*((w | ( Seg (n + 1))) . ( len (w | ( Seg (n + 1)))))*>) in ( succ t1) by A58, A63, TREES_2: 12;

              then

              consider k be Nat such that

               A68: (t1 ^ <*((w | ( Seg (n + 1))) . ( len (w | ( Seg (n + 1)))))*>) = (t1 ^ <*k*>) and

               A69: k in ( card ( NIC ((M /. (T1 . t1)),(T1 . t1)))) by A67;

              

               A70: ((w | ( Seg (n + 1))) . ( len (w | ( Seg (n + 1))))) in ( card ( NIC ((M /. (T2 . t2)),(T2 . t2)))) by A56, A57, A59, A64, A66, A68, A69, FINSEQ_2: 17, TREES_1: 20, XXREAL_0: 2;

              k = ((w | ( Seg (n + 1))) . ( len (w | ( Seg (n + 1))))) by A68, FINSEQ_2: 17;

              

              hence (T1 . (w | ( Seg (n + 1)))) = (( LocSeq (( NIC ((M /. (T1 . t1)),(T1 . t1))),S)) . ((w | ( Seg (n + 1))) . ( len (w | ( Seg (n + 1)))))) by A14, A63, A69

              .= (T2 . (w | ( Seg (n + 1)))) by A16, A56, A57, A59, A64, A66, A63, A70, TREES_1: 20, XXREAL_0: 2;

            end;

            

             A71: R[ 0 ] by A13, A15;

            for n be Nat holds R[n] from NAT_1:sch 2( A71, A55);

            then

             A72: (T1 . w) = (T2 . w) by A52, A54;

            

             A73: ( succ v) in U1 by A53;

            ( succ v) = { (v ^ <*k*>) where k be Nat : k in ( card ( NIC ((M /. (T1 . v)),(T1 . v)))) } & ( succ w) = { (w ^ <*k*>) where k be Nat : k in ( card ( NIC ((M /. (T2 . w)),(T2 . w)))) } by A14, A16;

            hence thesis by A48, A50, A52, A72, A73, TARSKI:def 4;

          end;

          (( dom T1) -level (n + 1)) = ( union U1) by TREES_9: 45;

          hence thesis by A21, TREES_9: 45;

        end;

        (( dom T1) -level 0 ) = { {} } by TREES_9: 44

        .= (( dom T2) -level 0 ) by TREES_9: 44;

        then

         A74: P[ 0 ];

        

         A75: for n be Nat holds P[n] from NAT_1:sch 2( A74, A17);

        for p be FinSequence of NAT st p in ( dom T1) holds (T1 qua Function . p) = (T2 qua Function . p)

        proof

          let p be FinSequence of NAT ;

          defpred P[ Nat] means $1 <= ( len p) & (p | ( Seg $1)) in ( dom T1) implies (T1 . (p | ( Seg $1))) = (T2 . (p | ( Seg $1)));

          

           A76: (p | ( Seg ( len p))) = p by FINSEQ_3: 49;

          

           A77: for n be Nat st P[n] holds P[(n + 1)]

          proof

            let n be Nat;

            assume that

             A78: P[n] and

             A79: (n + 1) <= ( len p) and

             A80: (p | ( Seg (n + 1))) in ( dom T1);

            set t1 = (p | ( Seg n));

            

             A81: 1 <= (n + 1) by NAT_1: 11;

            

             A82: ( len (p | ( Seg (n + 1)))) = (n + 1) by A79, FINSEQ_1: 17;

            then ( len (p | ( Seg (n + 1)))) in ( Seg (n + 1)) by A81, FINSEQ_1: 1;

            then

             A83: (p . (n + 1)) = ((p | ( Seg (n + 1))) . ( len (p | ( Seg (n + 1))))) by A82, FUNCT_1: 49;

            (n + 1) in ( dom p) by A79, A81, FINSEQ_3: 25;

            then

             A84: (p | ( Seg (n + 1))) = (t1 ^ <*((p | ( Seg (n + 1))) . ( len (p | ( Seg (n + 1)))))*>) by A83, FINSEQ_5: 10;

            

             A85: n <= (n + 1) by NAT_1: 11;

            then ( Seg n) c= ( Seg (n + 1)) by FINSEQ_1: 5;

            then (p | ( Seg n)) = ((p | ( Seg (n + 1))) | ( Seg n)) by RELAT_1: 74;

            then (p | ( Seg n)) is_a_prefix_of (p | ( Seg (n + 1))) by TREES_1:def 1;

            then

            reconsider t1 as Element of ( dom T1) by A80, TREES_1: 20;

            reconsider t2 = t1 as Element of ( dom T2) by A75, TREES_2: 38;

            

             A86: ( succ t1) = { (t1 ^ <*k*>) where k be Nat : k in ( card ( NIC ((M /. (T1 . t1)),(T1 . t1)))) } by A14;

            (t1 ^ <*((p | ( Seg (n + 1))) . ( len (p | ( Seg (n + 1)))))*>) in ( succ t1) by A80, A84, TREES_2: 12;

            then

            consider k be Nat such that

             A87: (t1 ^ <*((p | ( Seg (n + 1))) . ( len (p | ( Seg (n + 1)))))*>) = (t1 ^ <*k*>) and

             A88: k in ( card ( NIC ((M /. (T1 . t1)),(T1 . t1)))) by A86;

            

             A89: ((p | ( Seg (n + 1))) . ( len (p | ( Seg (n + 1))))) in ( card ( NIC ((M /. (T2 . t2)),(T2 . t2)))) by A78, A79, A85, A87, A88, FINSEQ_2: 17, XXREAL_0: 2;

            k = ((p | ( Seg (n + 1))) . ( len (p | ( Seg (n + 1))))) by A87, FINSEQ_2: 17;

            

            hence (T1 . (p | ( Seg (n + 1)))) = (( LocSeq (( NIC ((M /. (T1 . t1)),(T1 . t1))),S)) . ((p | ( Seg (n + 1))) . ( len (p | ( Seg (n + 1)))))) by A14, A84, A88

            .= (T2 . (p | ( Seg (n + 1)))) by A16, A78, A79, A85, A84, A89, XXREAL_0: 2;

          end;

          

           A90: P[ 0 ] by A13, A15;

          for n be Nat holds P[n] from NAT_1:sch 2( A90, A77);

          hence thesis by A76;

        end;

        hence thesis by A75, TREES_2: 31, TREES_2: 38;

      end;

    end

    theorem :: AMISTD_3:2

    for S be standard halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N holds ( ExecTree ( Stop S)) = ( TrivialInfiniteTree --> 0 )

    proof

      set D = TrivialInfiniteTree ;

      let S be standard halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;

      set M = ( Stop S);

      set E = ( ExecTree M);

      defpred R[ set] means (E . $1) in ( dom M);

      defpred X[ Nat] means (( dom E) -level $1) = (D -level $1);

      

       A2: (M . 0 ) = ( halt S) by FUNCOP_1: 72;

      

       A3: for t be Element of ( dom E) holds ( card ( NIC (( halt S),(E . t)))) = { 0 }

      proof

        let t be Element of ( dom E);

        reconsider Et = (E . t) as Nat;

        ( NIC (( halt S),Et)) = {Et} by AMISTD_1: 2;

        hence thesis by CARD_1: 30, CARD_1: 49;

      end;

      

       A4: for f be Element of ( dom E) st R[f] holds for a be Element of NAT st (f ^ <*a*>) in ( dom E) holds R[(f ^ <*a*>)]

      proof

        let f be Element of ( dom E) such that

         A5: R[f];

        

         A6: (M /. (E . f)) = (M . (E . f)) by A5, PARTFUN1:def 6;

        reconsider Ef = (E . f) as Nat;

        

         A7: (E . f) = 0 by A5, TARSKI:def 1;

        then ( NIC (( halt S),(E . f))) = { 0 } by AMISTD_1: 2;

        then ( canonical_isomorphism_of (( RelIncl ( order_type_of ( RelIncl ( NIC ((M /. (E . f)),(E . f)))))),( RelIncl ( NIC ((M /. (E . f)),(E . f)))))) = ( 0 .--> Ef) by A2, A7, A6, CARD_5: 38;

        

        then

         A8: (( canonical_isomorphism_of (( RelIncl ( order_type_of ( RelIncl ( NIC ((M /. (E . f)),(E . f)))))),( RelIncl ( NIC ((M /. (E . f)),(E . f)))))) . 0 ) = Ef by FUNCOP_1: 72

        .= 0 by A5, TARSKI:def 1;

        

         A9: ( card ( NIC (( halt S),(E . f)))) = { 0 } by A3;

        then

         A10: 0 in ( card ( NIC ((M /. (E . f)),(E . f)))) by A2, A7, A6, TARSKI:def 1;

        

         A11: ( succ f) = { (f ^ <*k*>) where k be Nat : k in ( card ( NIC ((M /. (E . f)),(E . f)))) } by Def2;

        

         A12: ( succ f) = {(f ^ <* 0 *>)}

        proof

          hereby

            let s be object;

            assume s in ( succ f);

            then

            consider k be Nat such that

             A13: s = (f ^ <*k*>) and

             A14: k in ( card ( NIC ((M /. (E . f)),(E . f)))) by A11;

            k = 0 by A2, A9, A7, A6, A14, TARSKI:def 1;

            hence s in {(f ^ <* 0 *>)} by A13, TARSKI:def 1;

          end;

          let s be object;

          assume s in {(f ^ <* 0 *>)};

          then s = (f ^ <* 0 *>) by TARSKI:def 1;

          hence thesis by A11, A10;

        end;

        let a be Element of NAT ;

        assume (f ^ <*a*>) in ( dom E);

        then (f ^ <*a*>) in ( succ f) by TREES_2: 12;

        then (f ^ <*a*>) = (f ^ <* 0 *>) by A12, TARSKI:def 1;

        

        then (E . (f ^ <*a*>)) = (( LocSeq (( NIC ((M /. (E . f)),(E . f))),S)) . 0 ) by A10, Def2

        .= 0 by A10, A8, Def1;

        hence thesis by TARSKI:def 1;

      end;

      (E . {} ) = ( FirstLoc M) by Def2;

      then

       A15: R[( <*> NAT )] by VALUED_1: 33;

      

       A16: for f be Element of ( dom E) holds R[f] from HILBERT2:sch 1( A15, A4);

      

       A17: for x be object st x in ( dom E) holds (E qua Function . x) = 0

      proof

        let x be object;

        assume x in ( dom E);

        then

        reconsider x as Element of ( dom E);

        (E . x) in ( dom M) by A16;

        hence thesis by TARSKI:def 1;

      end;

      

       A18: for n be Nat st X[n] holds X[(n + 1)]

      proof

        let n be Nat;

        set f0 = (n |-> 0 );

        set f1 = ((n + 1) |-> 0 );

        

         A19: (( dom E) -level (n + 1)) = { w where w be Element of ( dom E) : ( len w) = (n + 1) } by TREES_2:def 6;

        

         A20: ( len f1) = (n + 1) by CARD_1:def 7;

        assume

         A21: X[n];

        (( dom E) -level (n + 1)) = {f1}

        proof

          hereby

            let a be object;

            assume a in (( dom E) -level (n + 1));

            then

            consider t1 be Element of ( dom E) such that

             A22: a = t1 and

             A23: ( len t1) = (n + 1) by A19;

            reconsider t0 = (t1 | ( Seg n)) as Element of ( dom E) by RELAT_1: 59, TREES_1: 20;

            

             A24: ( succ t0) = { (t0 ^ <*k*>) where k be Nat : k in ( card ( NIC ((M /. (E . t0)),(E . t0)))) } by Def2;

            (E . t0) in ( dom M) by A16;

            then

             A25: (E . t0) = 0 by TARSKI:def 1;

            

             A26: ( card ( NIC (( halt S),(E . t0)))) = { 0 } & (M /. (E . t0)) = (M . (E . t0)) by A3, A16, PARTFUN1:def 6;

            then

             A27: 0 in ( card ( NIC ((M /. (E . t0)),(E . t0)))) by A2, A25, TARSKI:def 1;

            

             A28: ( succ t0) = {(t0 ^ <* 0 *>)}

            proof

              hereby

                let s be object;

                assume s in ( succ t0);

                then

                consider k be Nat such that

                 A29: s = (t0 ^ <*k*>) and

                 A30: k in ( card ( NIC ((M /. (E . t0)),(E . t0)))) by A24;

                k = 0 by A2, A25, A26, A30, TARSKI:def 1;

                hence s in {(t0 ^ <* 0 *>)} by A29, TARSKI:def 1;

              end;

              let s be object;

              assume s in {(t0 ^ <* 0 *>)};

              then s = (t0 ^ <* 0 *>) by TARSKI:def 1;

              hence thesis by A24, A27;

            end;

            (t1 . (n + 1)) is Nat & t1 = (t0 ^ <*(t1 . (n + 1))*>) by A23, FINSEQ_3: 55;

            then (t0 ^ <*(t1 . (n + 1))*>) in ( succ t0) by TREES_2: 12;

            then

             A31: (t0 ^ <*(t1 . (n + 1))*>) = (t0 ^ <* 0 *>) by A28, TARSKI:def 1;

            

             A32: n in NAT by ORDINAL1:def 12;

            n <= (n + 1) by NAT_1: 11;

            then ( Seg n) c= ( Seg (n + 1)) by FINSEQ_1: 5;

            then ( Seg n) c= ( dom t1) by A23, FINSEQ_1:def 3;

            then ( dom t0) = ( Seg n) by RELAT_1: 62;

            then (( dom E) -level n) = { w where w be Element of ( dom E) : ( len w) = n } & ( len t0) = n by FINSEQ_1:def 3, TREES_2:def 6, A32;

            then

             A33: t0 in (( dom E) -level n);

            

             A34: (( dom E) -level n) = {f0} by A21, TREES_2: 39;

            for k be Nat st 1 <= k & k <= ( len t1) holds (t1 . k) = (f1 . k)

            proof

              let k be Nat;

              assume 1 <= k & k <= ( len t1);

              then

               A35: k in ( Seg (n + 1)) by A23, FINSEQ_1: 1;

              now

                per cases by A35, FINSEQ_2: 7;

                  suppose

                   A36: k in ( Seg n);

                  

                  hence (t1 . k) = (t0 . k) by FUNCT_1: 49

                  .= (f0 . k) by A34, A33, TARSKI:def 1

                  .= 0 by A36, FUNCOP_1: 7;

                end;

                  suppose k = (n + 1);

                  hence (t1 . k) = 0 by A31, FINSEQ_2: 17;

                end;

              end;

              hence thesis by A35, FUNCOP_1: 7;

            end;

            then t1 = f1 by A20, A23, FINSEQ_1: 14;

            hence a in {f1} by A22, TARSKI:def 1;

          end;

          defpred P[ Nat] means ($1 |-> 0 ) in ( dom E);

          let a be object;

          

           A37: for n be Nat st P[n] holds P[(n + 1)]

          proof

            let n be Nat;

            assume P[n];

            then

            reconsider t = (n |-> 0 ) as Element of ( dom E);

            

             A38: ( succ t) = { (t ^ <*k*>) where k be Nat : k in ( card ( NIC ((M /. (E . t)),(E . t)))) } by Def2;

            (E . t) in ( dom M) by A16;

            then

             A39: (E . t) = 0 by TARSKI:def 1;

            ( card ( NIC (( halt S),(E . t)))) = { 0 } & (M /. (E . t)) = (M . (E . t)) by A3, A16, PARTFUN1:def 6;

            then 0 in ( card ( NIC ((M /. (E . t)),(E . t)))) by A2, A39, TARSKI:def 1;

            then (t ^ <* 0 *>) in ( succ t) by A38;

            then (t ^ <* 0 *>) in ( dom E);

            hence thesis by FINSEQ_2: 60;

          end;

          

           A40: P[ 0 ] by TREES_1: 22;

          for n be Nat holds P[n] from NAT_1:sch 2( A40, A37);

          then

           A41: f1 is Element of ( dom E);

          assume a in {f1};

          then a = f1 by TARSKI:def 1;

          hence thesis by A19, A20, A41;

        end;

        hence thesis by TREES_2: 39;

      end;

      (( dom E) -level 0 ) = { {} } by TREES_9: 44

      .= (D -level 0 ) by TREES_9: 44;

      then

       A42: X[ 0 ];

      for x be Nat holds X[x] from NAT_1:sch 2( A42, A18);

      then ( dom E) = D by TREES_2: 38;

      hence thesis by A17, FUNCOP_1: 11;

    end;